AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementGradientDerivativeSymmetry

- The derivative of a globally represented gradient field is symmetric at every point where that vector field is Frechet differentiable.

theorem isSymmetric_fderiv_of_gradient_field
    {phi : E → ℝ} {T : E → E} {A : E →L[ℝ] E} {x : E}
    (hphi : ∀ y, HasFDerivAt phi (innerSL ℝ (T y)) y)
    (hT : HasFDerivAt T A x) :
    A.IsSymmetric := by
  have hdual :
      HasFDerivAt (fun y => innerSL ℝ (T y)) ((innerSL ℝ).comp A) x := by
    simpa [Function.comp_def] using
      (innerSL ℝ).hasFDerivAt.comp x hT
  intro v w
  have hs := second_derivative_symmetric
    (f := phi)
    (f' := fun y => innerSL ℝ (T y))
    (f'' := (innerSL ℝ).comp A)
    hphi hdual v w
  change ⟪A v, w⟫ = ⟪v, A w⟫
  calc
    ⟪A v, w⟫ = ⟪A w, v⟫ := by simpa using hs
    _ = ⟪v, A w⟫ := real_inner_comm _ _

end DisplacementGradientDerivativeSymmetry
end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementGradientDerivativeSymmetry.lean:37published source at 0e31a3cda412