Comparison tools for ambient and intrinsic smooth gradients

import Definitions.Def_KLSModular_FunctionalInequalities_Energy_SmoothGradient_Intrinsic_Basic
import Mathlib.Analysis.Calculus.AddTorsor.AffineMap
import Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

noncomputable section
open MeasureTheory Filter Topology InnerProductSpace
open scoped ContDiff
namespace FunctionalInequalities
namespace Energy
namespace SmoothGradient
open Euclidean
universe u
 theorem norm_gradient_comp_le
    {X Y : Type*} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X]
    [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] [CompleteSpace Y]
    {f : Y → ℝ} {φ : X → Y} (hf : ContDiff ℝ ∞ f) (hφ : ContDiff ℝ ∞ φ)
    (hlip : LipschitzWith 1 φ) (x : X) :
    ‖gradient (f ∘ φ) x‖ ≤ ‖gradient f (φ x)‖ := by
  have hnorm : ‖fderiv ℝ φ x‖ ≤ 1 := norm_fderiv_le_of_lipschitz ℝ hlip
  calc
    ‖gradient (f ∘ φ) x‖ = ‖fderiv ℝ (f ∘ φ) x‖ := by
      rw [← toDual_gradient]
      exact ((toDual ℝ X).norm_map _).symm
    _ ≤ ‖fderiv ℝ f (φ x)‖ := by
      rw [fderiv_comp x (hf.differentiable (by simp) _) (hφ.differentiable (by simp) _)]
      exact (ContinuousLinearMap.opNorm_comp_le _ _).trans
        (by simpa using mul_le_mul_of_nonneg_left hnorm (norm_nonneg (fderiv ℝ f (φ x))))
    _ = ‖gradient f (φ x)‖ := by
      rw [← toDual_gradient]
      exact (toDual ℝ Y).norm_map _
 def pullbackTest
    {X Y : Type*} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X]
    [MeasurableSpace X] [BorelSpace X]
    [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] [CompleteSpace Y] [MeasurableSpace Y]
    {μ : ProbabilityMeasure X} {ν : ProbabilityMeasure Y} (f : Test ν)
    (φ : X → Y) (hφ : ContDiff ℝ ∞ φ) (hlip : LipschitzWith 1 φ)
    (hmp : MeasurePreserving φ (μ : Measure X) (ν : Measure Y)) : Test μ where
  toFun := f ∘ φ
  contDiff := f.contDiff.comp hφ
  memLp_two := f.memLp_two.comp_measurePreserving hmp
  gradient_sq_integrable := by
    apply (hmp.integrable_comp_of_integrable f.gradient_sq_integrable).mono'
    · have hc : Continuous (gradient (f ∘ φ)) :=
        (toDual ℝ X).symm.continuous.comp
          ((f.contDiff.comp hφ).continuous_fderiv (by simp))
      exact (hc.norm.pow 2).aestronglyMeasurable
    · filter_upwards with x
      rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)]
      exact pow_le_pow_left₀ (norm_nonneg _) (FunctionalInequalities.Energy.SmoothGradient.norm_gradient_comp_le f.contDiff hφ hlip x) 2
variable {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
  [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [FiniteDimensional ℝ E]
  (μ : ProbabilityMeasure E)
 def projectionCoordinates (x : E) : (Probability.affineSupport μ).direction :=
  (Probability.affineSupport μ).direction.orthogonalProjectionOnto
    (x - Probability.supportPoint μ)
end SmoothGradient
end Energy
end FunctionalInequalities