The Langevin Diffusion in Continuous Time

The proof applies Mathlib's one-sided Grönwall theorem to the negated interpolation and then cancels the positive exponential exactly.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem backward_interpolation_contraction_of_growth
    {interpolation interpolation' : ℝ → ℝ} {rate s t : ℝ}
    (hcontinuous : Continuous interpolation)
    (hderiv : ∀ u : ℝ,
      HasDerivWithinAt interpolation (interpolation' u) (Ici u) u)
    (hgrowth : ∀ u : ℝ,
      rate * interpolation u ≤ interpolation' u)
    (hst : s ≤ t) :
    interpolation s ≤
      interpolation t * Real.exp (-rate * (t - s)) := by
  have hbound : ∀ x ∈ Ico s t,
      -interpolation' x ≤ rate * (-interpolation x) + 0 := by
    intro x _hx
    have hneg := neg_le_neg (hgrowth x)
    simpa [neg_mul] using hneg
  have hgronwall :=
    le_gronwallBound_of_liminf_deriv_right_le
      (f := fun x => -interpolation x)
      (f' := fun x => -interpolation' x)
      (δ := -interpolation s)
      (K := rate)
      (ε := 0)
      (a := s)
      (b := t)
      hcontinuous.neg.continuousOn
      (fun x _hx r hr => by
        simpa [slope] using ((hderiv x).neg.liminf_right_slope_le hr))
      le_rfl
      hbound
      t
      ⟨hst, le_rfl⟩
  rw [gronwallBound_ε0] at hgronwall
  have hexponential_growth :
      interpolation s * Real.exp (rate * (t - s)) ≤ interpolation t := by
    linarith
  have hscaled := mul_le_mul_of_nonneg_right hexponential_growth
    (Real.exp_nonneg (-rate * (t - s)))
  have hinverse :
      Real.exp (rate * (t - s)) * Real.exp (-rate * (t - s)) = 1 := by
    rw [← Real.exp_add]
    have hzero : rate * (t - s) + -rate * (t - s) = 0 := by ring
    rw [hzero, Real.exp_zero]
  calc
    interpolation s =
        (interpolation s * Real.exp (rate * (t - s))) *
          Real.exp (-rate * (t - s)) := by
      rw [mul_assoc, hinverse, mul_one]
    _ ≤ interpolation t * Real.exp (-rate * (t - s)) := hscaled

Exact module and namespace context

The proof specializes the fully expanded curvature hypothesis and discharges the exact real-arithmetic consequence; no hidden definition is unfolded.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem interpolationDerivative_lower_bound_of_expandedBakryEmery
    (generator : (X → ℝ) →ₗ[ℝ] (X → ℝ))
    {alpha : ℝ} (_halpha : 0 < alpha)
    (hcurvature : ∀ (g : X → ℝ) (y : X),
      alpha * carreDuChamp generator g g y ≤
        (2 : ℝ)⁻¹ *
          (generator (carreDuChamp generator g g) y -
            carreDuChamp generator g (generator g) y -
            carreDuChamp generator g (generator g) y))
    (f : X → ℝ) (x : X) :
    2 * alpha * carreDuChamp generator f f x ≤
      generator (carreDuChamp generator f f) x -
        2 * carreDuChamp generator f (generator f) x := by
  have h := hcurvature f x
  nlinarith

end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

The proof derives the pointwise curvature bound, transfers it through each positive linear operator, and invokes the independently verified scalar backward interpolation theorem.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem backwardInterpolation_contraction_of_expandedBakryEmery
    (generator : (X → ℝ) →ₗ[ℝ] (X → ℝ))
    {alpha : ℝ} (halpha : 0 < alpha)
    (hcurvature : ∀ (g : X → ℝ) (y : X),
      alpha * carreDuChamp generator g g y ≤
        (2 : ℝ)⁻¹ *
          (generator (carreDuChamp generator g g) y -
            carreDuChamp generator g (generator g) y -
            carreDuChamp generator g (generator g) y))
    (evolution : ℝ → (X → ℝ) →ₗ[ℝ] (X → ℝ))
    (orbit : ℝ → X → ℝ) (x : X)
    (hpositive : ∀ u : ℝ, ∀ {f g : X → ℝ},
      (∀ y, f y ≤ g y) → ∀ z, evolution u f z ≤ evolution u g z)
    (hcontinuous : Continuous (fun u =>
      evolution u (carreDuChamp generator (orbit u) (orbit u)) x))
    (hderiv : ∀ u : ℝ,
      HasDerivWithinAt
        (fun v => evolution v
          (carreDuChamp generator (orbit v) (orbit v)) x)
        (evolution u
          (generator (carreDuChamp generator (orbit u) (orbit u)) -
            (2 : ℝ) • carreDuChamp generator (orbit u) (generator (orbit u))) x)
        (Ici u) u)
    {s t : ℝ} (hst : s ≤ t) :
    evolution s (carreDuChamp generator (orbit s) (orbit s)) x ≤
      evolution t (carreDuChamp generator (orbit t) (orbit t)) x *
        Real.exp (-(2 * alpha) * (t - s)) := by
  apply backward_interpolation_contraction_of_growth hcontinuous hderiv ?_ hst
  intro u
  let gamma : X → ℝ := carreDuChamp generator (orbit u) (orbit u)
  let mixed : X → ℝ :=
    carreDuChamp generator (orbit u) (generator (orbit u))
  have hpointwise : ∀ y,
      ((2 * alpha) • gamma) y ≤
        (generator gamma - (2 : ℝ) • mixed) y := by
    intro y
    simpa [gamma, mixed] using
      interpolationDerivative_lower_bound_of_expandedBakryEmery
        generator halpha hcurvature (orbit u) y
  have hmapped := hpositive u hpointwise x
  simpa [gamma, mixed] using hmapped

end

end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

The proof makes the exponentially weighted interpolation monotone and evaluates it at the two endpoints.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem backward_endpoint_contraction_of_growth_on_Icc
    {interpolation interpolation' : ℝ → ℝ} {rate s t : ℝ}
    (hst : s ≤ t)
    (hinterpolation : ∀ u ∈ Icc s t,
      HasDerivAt interpolation (interpolation' u) u)
    (hgrowth : ∀ u ∈ Ioo s t,
      rate * interpolation u ≤ interpolation' u) :
    interpolation s ≤
      interpolation t * Real.exp (-rate * (t - s)) := by
  let weighted : ℝ → ℝ := fun u =>
    interpolation u * Real.exp (-rate * (u - s))
  have hweighted : ∀ u ∈ Icc s t,
      HasDerivAt weighted
        ((interpolation' u - rate * interpolation u) *
          Real.exp (-rate * (u - s))) u := by
    intro u hu
    have hinner :
        HasDerivAt (fun v : ℝ => -rate * (v - s)) (-rate) u := by
      simpa using ((hasDerivAt_id u).sub_const s).const_mul (-rate)
    have hexp := (Real.hasDerivAt_exp (-rate * (u - s))).comp u hinner
    have hmul := (hinterpolation u hu).mul hexp
    change HasDerivAt
      (fun v => interpolation v * Real.exp (-rate * (v - s)))
      ((interpolation' u - rate * interpolation u) *
        Real.exp (-rate * (u - s))) u
    exact hmul.congr_deriv (by
      simp only [Function.comp_apply]
      ring)
  have hmono : MonotoneOn weighted (Icc s t) := by
    apply monotoneOn_of_deriv_nonneg (convex_Icc s t)
    · exact continuousOn_of_forall_continuousAt fun u hu =>
        (hweighted u hu).continuousAt
    · intro u hu
      exact (hweighted u (interior_subset hu)).differentiableAt.differentiableWithinAt
    · intro u hu
      rw [(hweighted u (interior_subset hu)).deriv]
      exact mul_nonneg (sub_nonneg.mpr
        (hgrowth u (by simpa only [interior_Icc] using hu)))
        (Real.exp_nonneg _)
  have hend := hmono ⟨le_rfl, hst⟩ ⟨hst, le_rfl⟩ hst
  simpa only [weighted, sub_self, mul_zero, Real.exp_zero, mul_one] using hend

end

end SemigroupDecay
end FunctionalInequalities
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

The proof transfers the existing L1 property of the stopped terminal representative through the library's completed random-stopping almost-everywhere identity.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem itoIntegralProcess_at_boundedStopping_integrable
    [IsFiniteMeasure mu]
    (eta : ProgressiveL2Integrand filtration mu T) (hT : 0 < T)
    (tau : Omega → ℝ≥0)
    (htau : IsChewiStoppingTime filtration
      (fun omega => (tau omega : WithTop ℝ≥0)))
    (htauT : ∀ omega, tau omega ≤ T)
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    (hUsual : SatisfiesUsualConditions filtration mu) :
    Integrable
      (fun omega => itoIntegralProcess eta hT hB hUsual (tau omega) omega) mu := by
  let _ : IsProbabilityMeasure mu := hB.isProbabilityMeasure
  let stoppedEta := stop eta (fun omega => (tau omega : WithTop ℝ≥0)) htau
  have hterminal :
      terminalRepresentative stoppedEta hT hB =ᵐ[mu]
        (fun omega => itoIntegralProcess eta hT hB hUsual (tau omega) omega) := by
    exact (itoIntegralTerminal_stop_ae eta hT tau htau htauT hB hUsual)
  exact (terminalRepresentative_integrable stoppedEta hT hB).congr hterminal

Exact module and namespace context

The proof applies deterministic-time preservation of martingale expectation to the stopped integrand and then rewrites the terminal value using the two existing almost-everywhere consistency theorems.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem integral_itoIntegralProcess_at_boundedStopping_eq_zero
    [IsFiniteMeasure mu]
    (eta : ProgressiveL2Integrand filtration mu T) (hT : 0 < T)
    (tau : Omega → ℝ≥0)
    (htau : IsChewiStoppingTime filtration
      (fun omega => (tau omega : WithTop ℝ≥0)))
    (htauT : ∀ omega, tau omega ≤ T)
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    (hUsual : SatisfiesUsualConditions filtration mu) :
    ∫ omega, itoIntegralProcess eta hT hB hUsual (tau omega) omega ∂mu = 0 := by
  let _ : IsProbabilityMeasure mu := hB.isProbabilityMeasure
  let stoppedEta := stop eta (fun omega => (tau omega : WithTop ℝ≥0)) htau
  have hmartingale :
      Martingale (itoIntegralProcess stoppedEta hT hB hUsual) filtration mu :=
    itoIntegralProcess_martingale stoppedEta hT hB hUsual
  have hterminalMean :
      ∫ omega, terminalRepresentative stoppedEta hT hB omega ∂mu = 0 := by
    have hmean := hmartingale.setIntegral_eq (show (0 : ℝ≥0) ≤ T from bot_le)
      (MeasurableSet.univ : MeasurableSet[filtration 0] Set.univ)
    have hprocessMean :
        ∫ omega, itoIntegralProcess stoppedEta hT hB hUsual T omega ∂mu = 0 := by
      simpa only [Measure.restrict_univ, itoIntegralProcess_at_zero,
        Pi.zero_apply, integral_zero] using hmean.symm
    exact integral_congr_ae
      (terminalRepresentative_ae_eq_actual stoppedEta hT hB hUsual) |>.trans hprocessMean
  calc
    ∫ omega, itoIntegralProcess eta hT hB hUsual (tau omega) omega ∂mu =
        ∫ omega, terminalRepresentative stoppedEta hT hB omega ∂mu := by
          apply integral_congr_ae
          exact (itoIntegralTerminal_stop_ae eta hT tau htau htauT hB hUsual).symm
    _ = 0 := hterminalMean

end BoundedStoppedItoMean
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

The proof rewrites the exact finite-grid second moment as 2T times the dyadic mesh and passes to the known zero-mesh limit.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem tendsto_integral_dyadic_quadraticVariationError_sq
    (hB : IsPreBrownianReal B mu) (T : ℝ≥0) :
    Tendsto
      (fun level =>
        ∫ omega,
          (quadraticVariationError B
            (regularGridTimes (dyadicMesh T level) (2 ^ level)) omega) ^ 2 ∂mu)
      atTop (nhds 0) := by
  have hexact : ∀ level : ℕ,
      (∫ omega,
          (quadraticVariationError B
            (regularGridTimes (dyadicMesh T level) (2 ^ level)) omega) ^ 2 ∂mu) =
        2 * (T : ℝ) * ((dyadicMesh T level : ℝ≥0) : ℝ) := by
    intro level
    rw [integral_quadraticVariationError_sq hB
      (regularGridTimes_monotone
        (dyadicMesh T level) (2 ^ level))]
    rw [sum_dyadic_cellLengths_sq]
    ring
  have hlimit := (FiniteTimeGrid.dyadicMesh_tendsto_zero T).const_mul (2 * (T : ℝ))
  have hfun :
      (fun level =>
        ∫ omega,
          (quadraticVariationError B
            (regularGridTimes (dyadicMesh T level) (2 ^ level)) omega) ^ 2 ∂mu) =
        fun level => 2 * (T : ℝ) * ((dyadicMesh T level : ℝ≥0) : ℝ) := by
    funext level
    exact hexact level
  rw [hfun]
  simpa using hlimit

end BrownianQuadraticVariationL2
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

The proof packages the Gaussian fourth-moment calculation into a one-cell variance, transports independence through the centered-square map, and invokes finite-sum variance additivity.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem integral_quadraticVariationError_sq
    (hB : IsPreBrownianReal B mu)
    {n : ℕ} {times : Fin (n + 1) → ℝ≥0}
    (hmono : Monotone times) :
    ∫ omega, (quadraticVariationError B times omega) ^ 2 ∂mu =
      2 * ∑ i : Fin n,
        (((times i.succ - times i.castSucc : ℝ≥0) : ℝ) ^ 2) := by
  let _ : IsProbabilityMeasure mu := hB.isGaussianProcess.isProbabilityMeasure
  let Y : Fin n → Omega → ℝ := fun i => centeredSquaredIncrement B times i
  have hYmem : ∀ i, MemLp (Y i) 2 mu := fun i => by
    change MemLp
      (fun omega =>
        (B (times i.succ) omega - B (times i.castSucc) omega) ^ 2 -
          ((times i.succ - times i.castSucc : ℝ≥0) : ℝ)) 2 mu
    simpa only using
      centered_increment_sq_memLp_two hB _ _
  have hYind : Set.Pairwise (↑(Finset.univ : Finset (Fin n)) : Set (Fin n))
      (fun i j => Y i ⟂ᵢ[mu] Y j) := by
    intro i _ j _ hij
    exact (iIndepFun_centeredSquaredIncrement hB hmono).indepFun hij
  have hvar := ProbabilityTheory.IndepFun.variance_sum
    (s := Finset.univ) (X := Y) (fun i _ => hYmem i) hYind
  have hsumMem : MemLp (∑ i : Fin n, Y i) 2 mu :=
    memLp_finsetSum' Finset.univ (fun i _ => hYmem i)
  have hmean : ∫ omega, (∑ i : Fin n, Y i) omega ∂mu = 0 := by
    calc
      ∫ omega, (∑ i : Fin n, Y i) omega ∂mu =
          ∫ omega, ∑ i ∈ (Finset.univ : Finset (Fin n)), Y i omega ∂mu := by
            congr 1
            funext omega
            simp only [Finset.sum_apply]
      _ = ∑ i ∈ (Finset.univ : Finset (Fin n)), ∫ omega, Y i omega ∂mu := by
        rw [integral_finsetSum]
        intro i _
        exact (hYmem i).integrable (by norm_num)
      _ = 0 := by
        apply Finset.sum_eq_zero
        intro i _
        simpa [Y, centeredSquaredIncrement] using
          integral_centered_increment_sq_eq_zero hB (grid_cell_le hmono i)
  rw [variance_of_integral_eq_zero hsumMem.aemeasurable hmean] at hvar
  change ∫ omega, (∑ i : Fin n, centeredSquaredIncrement B times i omega) ^ 2 ∂mu = _
  change ∫ omega, (∑ i : Fin n, Y i omega) ^ 2 ∂mu = _
  rw [show (∫ omega, (∑ i : Fin n, Y i omega) ^ 2 ∂mu) =
      ∑ i : Fin n, Var[Y i; mu] by
    simpa only [Finset.sum_apply] using hvar]
  rw [Finset.mul_sum]
  apply Finset.sum_congr rfl
  intro i _
  have hYiMean : ∫ omega, Y i omega ∂mu = 0 := by
    simpa [Y, centeredSquaredIncrement] using
      integral_centered_increment_sq_eq_zero hB (grid_cell_le hmono i)
  rw [variance_of_integral_eq_zero (hYmem i).aemeasurable hYiMean]
  simpa [Y, centeredSquaredIncrement] using
    integral_centered_increment_sq_sq hB (grid_cell_le hmono i)

Exact module and namespace context

The proof first derives integrability of the canonical llr from the admissible RN entropy integrand. It then applies the generator LSI to the canonical density and rewrites its two sides using Mathlib's RN/KL theorem and ASTIS's compiled Dirichlet--Fisher theorem.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem finite_klDiv_and_toReal_le_half_mul_information
    (mu pi : Measure (EuclideanSpace ℝ ι)) [IsProbabilityMeasure mu]
    [SigmaFinite mu] [Measure.HaveLebesgueDecomposition mu pi]
    (generator :
      (EuclideanSpace ℝ ι → ℝ) →ₗ[ℝ] (EuclideanSpace ℝ ι → ℝ))
    {C : ℝ}
    (hLSI : Generator.SatisfiesLogSobolev pi generator C)
    (hAdmissible : Generator.LogSobolevAdmissible pi generator
      (InformationTheory.RNLogRatio.density mu pi))
    (hScore :
      InformationTheory.CanonicalRelativeFisher.SmoothFiniteScoreDomain mu pi)
    (hPair :
      InformationTheory.CanonicalDirichletFisher.DirichletPairDomain
        mu pi generator)
    (hGamma :
      InformationTheory.CanonicalDirichletFisher.HasCanonicalFisherGamma
        mu pi generator) :
    _root_.InformationTheory.klDiv mu pi ≠ ∞ ∧
      (_root_.InformationTheory.klDiv mu pi).toReal ≤
        (C / 2) *
          InformationTheory.CanonicalRelativeFisher.information mu pi hScore := by
  let _ : IsProbabilityMeasure pi := hLSI.1
  have hLogRatioIntegrable : Integrable (MeasureTheory.llr mu pi) mu := by
    rw [← MeasureTheory.integrable_rnDeriv_mul_log_iff
      hScore.absolutelyContinuous]
    simpa [InformationTheory.RNLogRatio.density] using
      hAdmissible.2.2.2.1
  have hFinite : _root_.InformationTheory.klDiv mu pi ≠ ∞ :=
    _root_.InformationTheory.klDiv_ne_top
      hScore.absolutelyContinuous hLogRatioIntegrable
  refine ⟨hFinite, ?_⟩
  have hApplied := hLSI.2.2
    (InformationTheory.RNLogRatio.density mu pi) hAdmissible
  have hEntropy :
      Generator.densityEntropy pi
          (InformationTheory.RNLogRatio.density mu pi) =
        (_root_.InformationTheory.klDiv mu pi).toReal := by
    unfold Generator.densityEntropy
    change
      (∫ x, (mu.rnDeriv pi x).toReal *
        Real.log (mu.rnDeriv pi x).toReal ∂pi) =
        (_root_.InformationTheory.klDiv mu pi).toReal
    rw [MeasureTheory.integral_rnDeriv_mul_log
      hScore.absolutelyContinuous]
    simpa [InformationTheory.RNLogRatio.logRatio] using
      (InformationTheory.RNLogRatio.toReal_klDiv_eq_integral_logRatio_of_probability
        mu pi hScore.absolutelyContinuous).symm
  have hDirichlet :
      Generator.dirichletForm pi generator
          (InformationTheory.RNLogRatio.density mu pi)
          (fun x => Real.log
            (InformationTheory.RNLogRatio.density mu pi x)) =
        InformationTheory.CanonicalRelativeFisher.information mu pi hScore := by
    rw [show
      (fun x => Real.log (InformationTheory.RNLogRatio.density mu pi x)) =
        InformationTheory.RNLogRatio.logRatio mu pi by
      funext x
      exact (InformationTheory.RNLogRatio.logRatio_apply mu pi x).symm]
    exact
      InformationTheory.CanonicalDirichletFisher.dirichletForm_density_logRatio_eq_information
        mu pi generator hScore hPair hGamma
  rw [hEntropy, hDirichlet] at hApplied
  exact hApplied

end

end CanonicalLogSobolev
end FunctionalInequalities
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

This is a transparent definition; no theorem or probabilistic premise is hidden in it.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

def empiricalSecondMoment (sample : κ → E) : E →L[ℝ] E :=
  (Fintype.card κ : ℝ)⁻¹ •
    ∑ i, InnerProductSpace.rankOne ℝ (sample i) (sample i)

Exact module and namespace context

The proof uses the library norm formula and the definition of a square.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem norm_rankOne_self_eq_sq (x : E) :
    ‖InnerProductSpace.rankOne ℝ x x‖ = ‖x‖ ^ 2 := by
  simp [pow_two]

Exact module and namespace context

The proof performs the exact finite-sum cancellation, transports symmetry through subtraction, and combines the triangle inequality with the exact rank-one norm.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem empiricalSecondMoment_preconcentration
    [Nonempty κ]
    (population : E →L[ℝ] E) (sample : κ → E) (B : ℝ)
    (hB : 0 ≤ B)
    (hpopulationSymmetric : LinearMap.IsSymmetric (population : E →ₗ[ℝ] E))
    (hpopulationNorm : ‖population‖ ≤ B ^ 2)
    (hsampleNorm : ∀ i, ‖sample i‖ ≤ B) :
    (empiricalSecondMoment sample - population =
      (Fintype.card κ : ℝ)⁻¹ •
        ∑ i, (InnerProductSpace.rankOne ℝ (sample i) (sample i) - population)) ∧
    (∀ i, LinearMap.IsSymmetric
      ((InnerProductSpace.rankOne ℝ (sample i) (sample i) - population : E →L[ℝ] E) :
        E →ₗ[ℝ] E)) ∧
    (∀ i,
      ‖InnerProductSpace.rankOne ℝ (sample i) (sample i) - population‖ ≤
        2 * B ^ 2) := by
  have hcard : (Fintype.card κ : ℝ) ≠ 0 := by
    exact_mod_cast Fintype.card_ne_zero
  constructor
  · rw [Finset.sum_sub_distrib]
    unfold empiricalSecondMoment
    rw [smul_sub]
    congr 1
    rw [Finset.sum_const, ← Nat.cast_smul_eq_nsmul ℝ]
    exact (inv_smul_smul₀ hcard population).symm
  constructor
  · intro i
    exact (InnerProductSpace.isSymmetric_rankOne_self (sample i)).sub
      hpopulationSymmetric
  · intro i
    have hsample_sq : ‖sample i‖ ^ 2 ≤ B ^ 2 :=
      (sq_le_sq₀ (norm_nonneg (sample i)) hB).2 (hsampleNorm i)
    calc
      ‖InnerProductSpace.rankOne ℝ (sample i) (sample i) - population‖
          ≤ ‖InnerProductSpace.rankOne ℝ (sample i) (sample i)‖ + ‖population‖ :=
        norm_sub_le _ _
      _ = ‖sample i‖ ^ 2 + ‖population‖ := by
        rw [norm_rankOne_self_eq_sq]
      _ ≤ B ^ 2 + B ^ 2 := add_le_add hsample_sq hpopulationNorm
      _ = 2 * B ^ 2 := by ring

Exact module and namespace context

The proof integrates pointwise rank-one symmetry, applies the Bochner norm bound, expands the noncommutative centered square using rank-one idempotence, commutes multiplication through the integral, and finishes with the operator-norm triangle inequality.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem unitRankOneCovariance_momentPackage
    [CompleteSpace E]
    {Omega : Type*} [MeasurableSpace Omega]
    {mu : Measure Omega} [IsProbabilityMeasure mu]
    (sample : Omega → E) (population : E →L[ℝ] E)
    (hsampleUnit : ∀ omega, ‖sample omega‖ = 1)
    (hRankOneIntegrable :
      Integrable (fun omega =>
        InnerProductSpace.rankOne ℝ (sample omega) (sample omega)) mu)
    (hPopulation :
      ∫ omega, InnerProductSpace.rankOne ℝ (sample omega) (sample omega) ∂mu =
        population) :
    IsSelfAdjoint population ∧
      ‖population‖ ≤ 1 ∧
      (∫ omega,
          (InnerProductSpace.rankOne ℝ (sample omega) (sample omega) -
            population) ^ (2 : ℕ) ∂mu =
        population - population ^ (2 : ℕ)) ∧
      ‖population - population ^ (2 : ℕ)‖ ≤ 2 * ‖population‖ := by
  let A := E →L[ℝ] E
  have hSelfAdjoint : IsSelfAdjoint population := by
    rw [ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric]
    intro x y
    have hx : Integrable
        (fun omega =>
          (InnerProductSpace.rankOne ℝ (sample omega) (sample omega)) x) mu :=
      (ContinuousLinearMap.apply ℝ E x).integrable_comp hRankOneIntegrable
    have hy : Integrable
        (fun omega =>
          (InnerProductSpace.rankOne ℝ (sample omega) (sample omega)) y) mu :=
      (ContinuousLinearMap.apply ℝ E y).integrable_comp hRankOneIntegrable
    rw [← hPopulation]
    calc
      inner ℝ ((∫ omega,
          InnerProductSpace.rankOne ℝ (sample omega) (sample omega) ∂mu) x) y =
          inner ℝ (∫ omega,
            (InnerProductSpace.rankOne ℝ (sample omega) (sample omega)) x ∂mu) y := by
        rw [ContinuousLinearMap.integral_apply hRankOneIntegrable]
      _ = inner ℝ y (∫ omega,
            (InnerProductSpace.rankOne ℝ (sample omega) (sample omega)) x ∂mu) :=
        real_inner_comm _ _
      _ = ∫ omega,
            inner ℝ y
              ((InnerProductSpace.rankOne ℝ (sample omega) (sample omega)) x) ∂mu :=
        (integral_inner hx y).symm
      _ = ∫ omega,
            inner ℝ x
              ((InnerProductSpace.rankOne ℝ (sample omega) (sample omega)) y) ∂mu := by
        apply integral_congr_ae
        filter_upwards with omega
        calc
          inner ℝ y
              ((InnerProductSpace.rankOne ℝ (sample omega) (sample omega)) x) =
              inner ℝ
                ((InnerProductSpace.rankOne ℝ (sample omega) (sample omega)) x) y :=
            real_inner_comm _ _
          _ = inner ℝ x
                ((InnerProductSpace.rankOne ℝ (sample omega) (sample omega)) y) :=
            (InnerProductSpace.isSymmetric_rankOne_self
              (𝕜 := ℝ) (sample omega)) x y
      _ = inner ℝ x (∫ omega,
            (InnerProductSpace.rankOne ℝ (sample omega) (sample omega)) y ∂mu) :=
        integral_inner hy x
      _ = inner ℝ x ((∫ omega,
          InnerProductSpace.rankOne ℝ (sample omega) (sample omega) ∂mu) y) := by
        rw [ContinuousLinearMap.integral_apply hRankOneIntegrable]
  have hNorm : ‖population‖ ≤ 1 := by
    rw [← hPopulation]
    calc
      ‖∫ omega,
          InnerProductSpace.rankOne ℝ (sample omega) (sample omega) ∂mu‖ ≤
          1 * mu.real Set.univ := by
        apply norm_integral_le_of_norm_le_const
        filter_upwards with omega
        rw [norm_rankOne_self_eq_sq, hsampleUnit omega]
        norm_num
      _ = 1 := by simp
  have hright : Integrable
      (fun omega =>
        InnerProductSpace.rankOne ℝ (sample omega) (sample omega) * population) mu :=
    ((ContinuousLinearMap.mul ℝ A).flip population).integrable_comp
      hRankOneIntegrable
  have hleft : Integrable
      (fun omega =>
        population * InnerProductSpace.rankOne ℝ (sample omega) (sample omega)) mu :=
    (ContinuousLinearMap.mul ℝ A population).integrable_comp
      hRankOneIntegrable
  have hconst : Integrable (fun _ : Omega => population ^ (2 : ℕ)) mu :=
    integrable_const _
  have hSecondMoment :
      ∫ omega,
          (InnerProductSpace.rankOne ℝ (sample omega) (sample omega) -
            population) ^ (2 : ℕ) ∂mu =
        population - population ^ (2 : ℕ) := by
    calc
      (∫ omega,
          (InnerProductSpace.rankOne ℝ (sample omega) (sample omega) -
            population) ^ (2 : ℕ) ∂mu) =
          ∫ omega,
            InnerProductSpace.rankOne ℝ (sample omega) (sample omega) -
              InnerProductSpace.rankOne ℝ (sample omega) (sample omega) * population -
              population * InnerProductSpace.rankOne ℝ (sample omega) (sample omega) +
              population ^ (2 : ℕ) ∂mu := by
        apply integral_congr_ae
        filter_upwards with omega
        have hp := rankOne_self_sq_of_norm_one (sample omega) (hsampleUnit omega)
        calc
          (InnerProductSpace.rankOne ℝ (sample omega) (sample omega) -
              population) ^ (2 : ℕ) =
              (InnerProductSpace.rankOne ℝ (sample omega) (sample omega)) ^ (2 : ℕ) -
                InnerProductSpace.rankOne ℝ (sample omega) (sample omega) * population -
                population * InnerProductSpace.rankOne ℝ (sample omega) (sample omega) +
                population ^ (2 : ℕ) := by
            noncomm_ring
          _ = _ := by rw [hp]
      _ = (∫ omega,
            InnerProductSpace.rankOne ℝ (sample omega) (sample omega) ∂mu) -
            (∫ omega,
              InnerProductSpace.rankOne ℝ (sample omega) (sample omega) * population ∂mu) -
            (∫ omega,
              population * InnerProductSpace.rankOne ℝ (sample omega) (sample omega) ∂mu) +
            (∫ _ : Omega, population ^ (2 : ℕ) ∂mu) := by
        have hthree :
            (∫ omega,
              InnerProductSpace.rankOne ℝ (sample omega) (sample omega) -
                InnerProductSpace.rankOne ℝ (sample omega) (sample omega) * population -
                population * InnerProductSpace.rankOne ℝ (sample omega) (sample omega) ∂mu) =
              (∫ omega,
                InnerProductSpace.rankOne ℝ (sample omega) (sample omega) ∂mu) -
              (∫ omega,
                InnerProductSpace.rankOne ℝ (sample omega) (sample omega) * population ∂mu) -
              (∫ omega,
                population * InnerProductSpace.rankOne ℝ (sample omega) (sample omega) ∂mu) := by
          have houter := integral_sub (hRankOneIntegrable.sub hright) hleft
          have hinner := integral_sub hRankOneIntegrable hright
          calc
            (∫ omega,
                InnerProductSpace.rankOne ℝ (sample omega) (sample omega) -
                  InnerProductSpace.rankOne ℝ (sample omega) (sample omega) * population -
                  population * InnerProductSpace.rankOne ℝ (sample omega) (sample omega) ∂mu) =
                (∫ omega,
                  InnerProductSpace.rankOne ℝ (sample omega) (sample omega) -
                    InnerProductSpace.rankOne ℝ (sample omega) (sample omega) * population ∂mu) -
                (∫ omega,
                  population * InnerProductSpace.rankOne ℝ (sample omega) (sample omega) ∂mu) := by
              simpa only [Pi.sub_apply] using houter
            _ = _ := by rw [hinner]
        have hadd := integral_add
          (hRankOneIntegrable.sub hright |>.sub hleft) hconst
        calc
          (∫ omega,
              InnerProductSpace.rankOne ℝ (sample omega) (sample omega) -
                InnerProductSpace.rankOne ℝ (sample omega) (sample omega) * population -
                population * InnerProductSpace.rankOne ℝ (sample omega) (sample omega) +
                population ^ (2 : ℕ) ∂mu) =
              (∫ omega,
                InnerProductSpace.rankOne ℝ (sample omega) (sample omega) -
                  InnerProductSpace.rankOne ℝ (sample omega) (sample omega) * population -
                  population * InnerProductSpace.rankOne ℝ (sample omega) (sample omega) ∂mu) +
              (∫ _ : Omega, population ^ (2 : ℕ) ∂mu) := by
            simpa only [Pi.add_apply, Pi.sub_apply] using hadd
          _ = _ := by rw [hthree]
      _ = population - population ^ (2 : ℕ) := by
        have hrightInt :
            (∫ omega,
              InnerProductSpace.rankOne ℝ (sample omega) (sample omega) * population ∂mu) =
              (∫ omega,
                InnerProductSpace.rankOne ℝ (sample omega) (sample omega) ∂mu) *
                population := by
          simpa [A, mul_apply_eq_comp] using
            ContinuousLinearMap.integral_comp_comm
              ((ContinuousLinearMap.mul ℝ A).flip population)
              hRankOneIntegrable
        have hleftInt :
            (∫ omega,
              population * InnerProductSpace.rankOne ℝ (sample omega) (sample omega) ∂mu) =
              population *
                (∫ omega,
                  InnerProductSpace.rankOne ℝ (sample omega) (sample omega) ∂mu) := by
          simpa [A, mul_apply_eq_comp] using
            ContinuousLinearMap.integral_comp_comm
              (ContinuousLinearMap.mul ℝ A population) hRankOneIntegrable
        rw [hPopulation, hrightInt, hleftInt]
        simp [hPopulation]
        noncomm_ring
  have hVariance :
      ‖population - population ^ (2 : ℕ)‖ ≤ 2 * ‖population‖ := by
    calc
      ‖population - population ^ (2 : ℕ)‖ ≤
          ‖population‖ + ‖population ^ (2 : ℕ)‖ := norm_sub_le _ _
      _ ≤ ‖population‖ + ‖population‖ ^ (2 : ℕ) := by
        gcongr
        exact norm_pow_le' _ (by norm_num)
      _ ≤ 2 * ‖population‖ := by
        nlinarith [norm_nonneg population]
  exact ⟨hSelfAdjoint, hNorm, hSecondMoment, hVariance⟩

end EmpiricalCovariance
end Probability
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

The proof differentiates the exact comparison primitive and applies Mathlib's derivative monotonicity theorem.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem endpoint_le_of_deriv_le_exponential_kernel
    {H H' : ℝ → ℝ} {rate source t energy : ℝ}
    (hrate : 0 < rate) (ht : 0 ≤ t)
    (hH : ∀ s ∈ Icc (0 : ℝ) t, HasDerivAt H (H' s) s)
    (hzero : H 0 = 0)
    (hderiv : ∀ s ∈ Ioo (0 : ℝ) t,
      H' s ≤ source * Real.exp (-rate * (t - s)) * energy) :
    H t ≤ (source / rate) * (1 - Real.exp (-rate * t)) * energy := by
  let B : ℝ → ℝ := fun s =>
    (source / rate) *
      (Real.exp (-rate * (t - s)) - Real.exp (-rate * t)) * energy
  have hB : ∀ s : ℝ,
      HasDerivAt B
        (source * Real.exp (-rate * (t - s)) * energy) s := by
    intro s
    have hinner : HasDerivAt (fun u : ℝ => -rate * (t - u)) rate s := by
      have hcoeff : -(-rate) = rate := by ring
      simpa only [Pi.sub_apply, id_eq, zero_sub, mul_neg, mul_one, hcoeff] using
        (((hasDerivAt_const s t).sub (hasDerivAt_id s)).const_mul (-rate))
    have hexp := (Real.hasDerivAt_exp (-rate * (t - s))).comp s hinner
    have hsub := hexp.sub_const (Real.exp (-rate * t))
    have hmul := (hsub.const_mul (source / rate)).mul_const energy
    convert hmul using 1 <;> try rfl
    field_simp [ne_of_gt hrate]
  have hmono : MonotoneOn (fun s => B s - H s) (Icc (0 : ℝ) t) := by
    apply monotoneOn_of_deriv_nonneg (convex_Icc (0 : ℝ) t)
    · exact continuousOn_of_forall_continuousAt fun s hs =>
        ((hB s).sub (hH s hs)).continuousAt
    · intro s hs
      exact ((hB s).sub (hH s (interior_subset hs))).differentiableAt.differentiableWithinAt
    · intro s hs
      change 0 ≤ deriv (B - H) s
      rw [((hB s).sub (hH s (interior_subset hs))).deriv]
      exact sub_nonneg.mpr (hderiv s (by simpa only [interior_Icc] using hs))
  have hend := hmono ⟨le_rfl, ht⟩ ⟨ht, le_rfl⟩ ht
  dsimp [B] at hend
  have hBzero :
      (source / rate) *
        (Real.exp (-rate * (t - 0)) - Real.exp (-rate * t)) * energy = 0 := by
    ring_nf
  rw [hBzero, hzero] at hend
  have hBt :
      (source / rate) *
        (Real.exp (-rate * (t - t)) - Real.exp (-rate * t)) * energy =
      (source / rate) * (1 - Real.exp (-rate * t)) * energy := by
    rw [sub_self, mul_zero, Real.exp_zero]
  rw [hBt] at hend
  exact sub_nonneg.mp (by simpa only [sub_self] using hend)

end

end AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities

Exact module and namespace context

The proof is a direct specialization of Mathlib's one-sided Grönwall theorem, followed by exact field algebra.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem forced_exponential_decay_of_scaled_dissipation_from
    {scale rate forcing : ℝ} (hrate : 0 < rate)
    (curve : DissipationCurve scale)
    (hcoercive : ∀ u : ℝ,
      rate * curve.energy u ≤ scale * curve.dissipation u + forcing)
    {s t : ℝ} (hst : s ≤ t) :
    curve.energy t ≤
      curve.energy s * Real.exp (-rate * (t - s)) +
        (forcing / rate) * (1 - Real.exp (-rate * (t - s))) := by
  have hbound : ∀ x ∈ Ico s t,
      -scale * curve.dissipation x ≤
        (-rate) * curve.energy x + forcing := by
    intro x _hx
    have hneg := neg_le_neg (hcoercive x)
    linarith
  have hgronwall :=
    le_gronwallBound_of_liminf_deriv_right_le
      (f := curve.energy)
      (f' := fun x => -scale * curve.dissipation x)
      (δ := curve.energy s)
      (K := -rate)
      (ε := forcing)
      (a := s)
      (b := t)
      curve.energy_continuous.continuousOn
      (fun x _hx r hr => by
        simpa [slope] using
          (curve.energy_hasDerivWithinAt x).liminf_right_slope_le hr)
      le_rfl
      hbound
      t
      ⟨hst, le_rfl⟩
  rw [gronwallBound] at hgronwall
  simp only [if_neg (neg_ne_zero.mpr hrate.ne')] at hgronwall
  calc
    curve.energy t ≤
        curve.energy s * Real.exp (-rate * (t - s)) +
          forcing / -rate *
            (Real.exp (-rate * (t - s)) - 1) := hgronwall
    _ = curve.energy s * Real.exp (-rate * (t - s)) +
          (forcing / rate) *
            (1 - Real.exp (-rate * (t - s))) := by
      field_simp [hrate.ne']
      ring

end

end SemigroupDecay
end FunctionalInequalities
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

The formula proof above explains the mathematical moves; the adjacent folded Lean gives their exact implementation.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem continuous_gaussian_polynomial_ridge_L2
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (p : Polynomial ℝ) :
    ∃ hfeature : ∀ w : {w : E // ‖w‖ = 1},
      MemLp (fun x : E => p.eval ⟪w.1, x⟫_ℝ) 2 (ProbabilityTheory.stdGaussian E),
      Continuous (fun w : {w : E // ‖w‖ = 1} =>
        (hfeature w).toLp (fun x : E => p.eval ⟪w.1, x⟫_ℝ)) := by
  classical
  letI : CompleteSpace E := FiniteDimensional.complete ℝ E
  letI : SecondCountableTopology E := inferInstance
  let μ := stdGaussian E
  obtain ⟨B,hB,hBpos,hBbound⟩ := polynomial_norm_envelope (E := E) p
  obtain ⟨hb, hbpos, hf, hnorm⟩ :=
    AutoSamplingTheory.TechnicalLemmas.Probability.GaussianPolynomialRidge.standard_gaussian_polynomial_ridge_uniform_L2 (E := E) p
  refine ⟨hf, ?_⟩
  let F := fun w : {w : E // ‖w‖ = 1} => (hf w).toLp (fun x => p.eval ⟪w.1,x⟫_ℝ)
  change Continuous F
  apply continuous_iff_continuousAt.2
  intro w₀
  have hBsq : Integrable (fun x => 4 * (B x)^2) μ :=
    ((memLp_two_iff_integrable_sq hB.1).1 hB).const_mul 4
  have hn (w) : ‖F w - F w₀‖^2 =
      ∫ x, (p.eval ⟪w.1,x⟫_ℝ - p.eval ⟪w₀.1,x⟫_ℝ)^2 ∂μ := by
    rw [← real_inner_self_eq_norm_sq, L2.inner_def]
    apply integral_congr_ae
    filter_upwards [Lp.coeFn_sub (F w) (F w₀), (hf w).coeFn_toLp, (hf w₀).coeFn_toLp] with x hx hw hw₀
    simp only [hx, Pi.sub_apply, F] at *
    rw [hw,hw₀]
    simp [real_inner_self_eq_norm_sq, Real.norm_eq_abs, sq_abs]
  have hc : ContinuousAt (fun w : {w : E // ‖w‖ = 1} =>
      ∫ x, (p.eval ⟪w.1,x⟫_ℝ - p.eval ⟪w₀.1,x⟫_ℝ)^2 ∂μ) w₀ := by
    apply continuousAt_of_dominated (bound := fun x => 4 * (B x)^2)
    · exact Eventually.of_forall fun w => by fun_prop
    · exact Eventually.of_forall fun w => ae_of_all _ fun x => by
        rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)]
        have h := (norm_sub_le (p.eval ⟪w.1,x⟫_ℝ) (p.eval ⟪w₀.1,x⟫_ℝ)).trans
          (add_le_add (hBbound w x) (hBbound w₀ x))
        have hs := (sq_le_sq₀ (norm_nonneg _) (add_nonneg (hBpos x) (hBpos x))).2 h
        simpa only [Real.norm_eq_abs, sq_abs] using hs.trans_eq (by ring)
    · exact hBsq
    · exact ae_of_all _ fun x => by fun_prop
  have hsq : ContinuousAt (fun w => ‖F w - F w₀‖^2) w₀ := by
    simpa only [← hn] using hc
  rw [ContinuousAt, tendsto_iff_dist_tendsto_zero]
  simpa only [Function.comp_def, Real.sqrt_sq (norm_nonneg _), sub_self, norm_zero, zero_pow (by decide : 2 ≠ 0),
    Real.sqrt_zero, dist_eq_norm] using
    (Real.continuous_sqrt.continuousAt.comp hsq).tendsto

Exact module and namespace context

The formula proof above explains the mathematical moves; the adjacent folded Lean gives their exact implementation.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem gaussian_polynomial_parameter_average_L2
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (p : Polynomial ℝ) :
    ∃ hfeature : ∀ w : {w : E // ‖w‖ = 1},
      MemLp (fun x : E => p.eval ⟪w.1, x⟫_ℝ) 2 (ProbabilityTheory.stdGaussian E),
      Continuous (fun w : {w : E // ‖w‖ = 1} =>
        (hfeature w).toLp (fun x : E => p.eval ⟪w.1, x⟫_ℝ)) ∧
      ∀ rho : Measure {w : E // ‖w‖ = 1}, IsProbabilityMeasure rho →
        (∀ x : E, Integrable (fun w : {w : E // ‖w‖ = 1} => p.eval ⟪w.1, x⟫_ℝ) rho) ∧
        Integrable (fun w : {w : E // ‖w‖ = 1} =>
          (hfeature w).toLp (fun x : E => p.eval ⟪w.1, x⟫_ℝ)) rho ∧
        ∃ hmean : MemLp (fun x : E => ∫ w : {w : E // ‖w‖ = 1},
            p.eval ⟪w.1, x⟫_ℝ ∂rho) 2 (ProbabilityTheory.stdGaussian E),
          hmean.toLp (fun x : E => ∫ w : {w : E // ‖w‖ = 1}, p.eval ⟪w.1, x⟫_ℝ ∂rho) =
            ∫ w : {w : E // ‖w‖ = 1},
              (hfeature w).toLp (fun x : E => p.eval ⟪w.1, x⟫_ℝ) ∂rho := by
  classical
  letI : CompleteSpace E := FiniteDimensional.complete ℝ E
  letI : SecondCountableTopology E := inferInstance
  let μ := stdGaussian E
  obtain ⟨B,hB,hBpos,hBbound⟩ := polynomial_norm_envelope (E := E) p
  obtain ⟨hf,hcont⟩ := AutoSamplingTheory.TechnicalLemmas.Probability.GaussianPolynomialAveraging.continuous_gaussian_polynomial_ridge_L2 (E := E) p
  obtain ⟨hb, hbpos, hf8, hnorm⟩ :=
    AutoSamplingTheory.TechnicalLemmas.Probability.GaussianPolynomialRidge.standard_gaussian_polynomial_ridge_uniform_L2 (E := E) p
  let U := {w : E // ‖w‖ = 1}
  let K : U → E → ℝ := fun w x => p.eval ⟪w.1,x⟫_ℝ
  let F := fun w : U => (hf w).toLp (K w)
  have hFcont : Continuous F := hcont
  have hFbound (w : U) : ‖F w‖ ≤ ‖hb.toLp (fun z : ℝ => p.eval z)‖ + 1 :=
    (hnorm w).2
  have hKcont : Continuous (fun z : U × E => K z.1 z.2) := by
    change Continuous (fun z : {w : E // ‖w‖ = 1} × E => p.eval ⟪z.1.1,z.2⟫_ℝ)
    fun_prop
  refine ⟨hf, hcont, ?_⟩
  intro rho hrho
  letI : IsProbabilityMeasure rho := hrho
  have hscalar (x : E) : Integrable (fun w : U => K w x) rho := by
    apply (integrable_const (B x)).mono' (by fun_prop)
    exact ae_of_all _ fun w => hBbound w x
  have hFint : Integrable F rho := by
    apply (integrable_const (‖hb.toLp (fun z : ℝ => p.eval z)‖ + 1)).mono'
      hFcont.aestronglyMeasurable
    exact ae_of_all _ hFbound
  let mean : E → ℝ := fun x => ∫ w, K w x ∂rho
  have hmeanmeas : StronglyMeasurable mean :=
    hKcont.stronglyMeasurable.integral_prod_left'
  have hmeanbound (x : E) : ‖mean x‖ ≤ B x := by
    have h := norm_integral_le_of_norm_le_const (μ := rho) (f := fun w : U => K w x)
      (ae_of_all _ fun w => hBbound w x)
    simpa only [probReal_univ, mul_one] using h
  have hmean : MemLp mean 2 μ := hB.mono' hmeanmeas.aestronglyMeasurable
    (ae_of_all _ hmeanbound)
  refine ⟨hscalar,hFint,hmean,?_⟩
  apply ext_inner_left ℝ
  intro g
  have hC : Integrable (fun x : E => ‖g x‖ * B x) μ :=
    (Lp.memLp g).norm.integrable_mul hB
  have hHmeas : AEStronglyMeasurable (fun z : U × E => g z.2 * K z.1 z.2) (rho.prod μ) :=
    (Lp.aestronglyMeasurable g).comp_snd.mul hKcont.aestronglyMeasurable
  have hHint : Integrable (fun z : U × E => g z.2 * K z.1 z.2) (rho.prod μ) := by
    apply (hC.comp_snd rho).mono' hHmeas
    exact ae_of_all _ fun z => by
      rw [norm_mul]
      exact mul_le_mul_of_nonneg_left (hBbound z.1 z.2) (norm_nonneg _)
  have hin (w : U) : ⟪g,F w⟫_ℝ = ∫ x, g x * K w x ∂μ := by
    rw [L2.inner_def]
    apply integral_congr_ae
    filter_upwards [(hf w).coeFn_toLp] with x hx
    change inner ℝ (g x) ((hf w).toLp (K w) x) = _
    rw [hx]
    simp only [RCLike.inner_apply, conj_trivial, K, mul_comm]
  calc
    ⟪g,hmean.toLp mean⟫_ℝ = ∫ x, g x * mean x ∂μ := by
      rw [L2.inner_def]
      apply integral_congr_ae
      filter_upwards [hmean.coeFn_toLp] with x hx
      rw [hx]
      simp only [RCLike.inner_apply, conj_trivial, K, mul_comm]
    _ = ∫ x, ∫ w, g x * K w x ∂rho ∂μ := by
      apply integral_congr_ae
      exact ae_of_all _ fun x => (integral_const_mul (g x) (fun w : U => K w x)).symm
    _ = ∫ w, ∫ x, g x * K w x ∂μ ∂rho := (integral_integral_swap hHint).symm
    _ = ∫ w, ⟪g,F w⟫_ℝ ∂rho := integral_congr_ae (ae_of_all _ fun w => (hin w).symm)
    _ = ⟪g,∫ w, F w ∂rho⟫_ℝ := integral_inner hFint g

end AutoSamplingTheory.TechnicalLemmas.Probability.GaussianPolynomialAveraging

Exact module and namespace context

See the adjacent exact Lean and the four mathematical proof steps.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem standard_gaussian_polynomial_ridge_uniform_L2
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (p : Polynomial ℝ) :
    let phi : ℝ → ℝ := fun z => p.eval z
    ∃ hbase : MemLp phi 2 (ProbabilityTheory.gaussianReal 0 1),
      let b : ℝ := ‖hbase.toLp phi‖ + 1
      (0 < b) ∧
      ∃ hfeature : ∀ w : {w : E // ‖w‖ = 1},
        MemLp (fun x : E => phi ⟪w.1, x⟫_ℝ) 2 (ProbabilityTheory.stdGaussian E),
        ∀ w : {w : E // ‖w‖ = 1},
          ‖(hfeature w).toLp (fun x : E => phi ⟪w.1, x⟫_ℝ)‖ = ‖hbase.toLp phi‖ ∧
          ‖(hfeature w).toLp (fun x : E => phi ⟪w.1, x⟫_ℝ)‖ ≤ b := by
  let phi : ℝ → ℝ := fun z => p.eval z
  have hpow : ∀ n : ℕ,
      MemLp (fun z : ℝ => z ^ n) 2 (gaussianReal 0 1) := by
    intro n
    apply (memLp_two_iff_integrable_sq (by fun_prop)).2
    have hid : MemLp (id : ℝ → ℝ) (↑(2 * n) : ℝ≥0∞) (gaussianReal 0 1) :=
      memLp_id_gaussianReal' (↑(2 * n) : ℝ≥0∞) (ENNReal.natCast_ne_top (2 * n))
    have hi := hid.integrable_norm_pow' (p := 2 * n)
    convert hi using 1
    funext z
    change (z ^ n) ^ 2 = ‖z‖ ^ (2 * n)
    rw [Nat.mul_comm 2 n, pow_mul, ← norm_pow, Real.norm_eq_abs, sq_abs]
  have hbase : MemLp phi 2 (gaussianReal 0 1) := by
    change MemLp (fun z : ℝ => p.eval z) 2 (gaussianReal 0 1)
    induction p using Polynomial.induction_on' with
    | add p q hp hq => simpa only [Polynomial.eval_add, Pi.add_def] using hp.add hq
    | monomial n a => simpa only [Polynomial.eval_monomial] using (hpow n).const_mul a
  have hmap : ∀ w : {w : E // ‖w‖ = 1},
      (stdGaussian E).map (fun x : E => ⟪w.1, x⟫_ℝ) = gaussianReal 0 1 := by
    intro w
    change (stdGaussian E).map (innerSL ℝ w.1) = _
    rw [IsGaussian.map_eq_gaussianReal, integral_strongDual_stdGaussian,
      variance_dual_stdGaussian, innerSL_apply_norm, w.2]
    norm_num
  let mp : ∀ w : {w : E // ‖w‖ = 1},
      MeasurePreserving (fun x : E => ⟪w.1, x⟫_ℝ) (stdGaussian E) (gaussianReal 0 1) :=
    fun w => ⟨by fun_prop, hmap w⟩
  let hfeature : ∀ w : {w : E // ‖w‖ = 1},
      MemLp (fun x : E => phi ⟪w.1, x⟫_ℝ) 2 (stdGaussian E) :=
    fun w => hbase.comp_measurePreserving (mp w)
  refine ⟨hbase, ?_, hfeature, ?_⟩
  · exact add_pos_of_nonneg_of_pos (norm_nonneg _) zero_lt_one
  · intro w
    have hn : ‖(hfeature w).toLp (fun x : E => phi ⟪w.1, x⟫_ℝ)‖ = ‖hbase.toLp phi‖ := by
      change ‖Lp.compMeasurePreserving (fun x : E => ⟪w.1, x⟫_ℝ) (mp w)
        (hbase.toLp phi)‖ = ‖hbase.toLp phi‖
      exact Lp.norm_compMeasurePreserving _ _
    exact ⟨hn, hn.trans_le (le_add_of_nonneg_right zero_le_one)⟩

end AutoSamplingTheory.TechnicalLemmas.Probability.GaussianPolynomialRidge

Exact module and namespace context