Fundamental lemma of the calculus of variations #
The key took in variational calculus is:
∀ h, ∫ x, f x * h x = 0 → f = 0
which allows use to go from reasoning about integrals to reasoning about functions. There are
theorem
fundamental_theorem_of_variational_calculus
{X : Type u_1}
[NormedAddCommGroup X]
[NormedSpace ℝ X]
[MeasurableSpace X]
{V : Type u_2}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[InnerProductSpace' ℝ V]
{f : X → V}
(μ : MeasureTheory.Measure X)
[MeasureTheory.IsFiniteMeasureOnCompacts μ]
[μ.IsOpenPosMeasure]
[OpensMeasurableSpace X]
(hf : IsTestFunction f)
(hg : ∀ (g : X → V), IsTestFunction g → ∫ (x : X), inner ℝ (f x) (g x) ∂μ = 0)
:
theorem
fundamental_theorem_of_variational_calculus'
{X : Type u_1}
[NormedAddCommGroup X]
[NormedSpace ℝ X]
[MeasurableSpace X]
{V : Type u_2}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[InnerProductSpace' ℝ V]
{f : X → V}
(μ : MeasureTheory.Measure X)
[MeasureTheory.IsFiniteMeasureOnCompacts μ]
[μ.IsOpenPosMeasure]
[OpensMeasurableSpace X]
(hf : Continuous f)
(hg : ∀ (g : X → V), IsTestFunction g → ∫ (x : X), inner ℝ (f x) (g x) ∂μ = 0)
:
The assumption IsTestFunction f in fundamental_theorem_of_variational_calculus can be
weakened to Continuous f.
The proof is by contradiction, assume that there is x₀ such that f x₀ then you can easily
construct g test function with support on the neighborhood of x₀ such that ⟪f x, g x⟫ ≥ 0.