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.

theorem fundamental_theorem_of_variational_calculus' {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [InnerProductSpace' ℝ V] {Y : Type u_1} [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] [FiniteDimensional ℝ Y] [MeasurableSpace Y] {f : Y → V} (μ : MeasureTheory.Measure Y) [MeasureTheory.IsFiniteMeasureOnCompacts μ] [μ.IsOpenPosMeasure] [OpensMeasurableSpace Y] (hf : Continuous f) (hg : ∀ (g : Y → V), IsTestFunction g → ∫ (x : Y), inner ℝ (f x) (g x) ∂μ = 0) : f = 0

A version of fundamental_theorem_of_variational_calculus' for Continuous f. The proof uses assumption that source of f is finite-dimensional inner-product space, so that a bump function with compact support exists via ContDiffBump.hasCompactSupport from Analysis.Calculus.BumpFunction.Basic.

The proof is by contradiction, assume that there is x₀ such that f x₀ ≠ 0 then one construct construct g test function supported on the neighborhood of x₀ such that ⟪f x, g x⟫ ≥ 0 and ⟪f x, g x⟫ > 0 on a neighborhood of x₀.

Using Y for the theorem below to make use of bump functions in InnerProductSpaces. Y is a finite dimensional measurable space over ℝ with (standard) inner product.

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) : f = 0