Closability of the Malliavin derivative (Solution)

This module repeats the Mathlib-only statement boundary from Challenge and discharges the advertised theorem using the development in Malliavin. The boundary definitions remain explicit for independent statement auditing; IsSmoothBounded.toMalliavin transfers their witnesses to the shared library API.

noncomputable def CameronMartin.Space {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] [BorelSpace W] (μ : MeasureTheory.Measure W) [ProbabilityTheory.IsGaussian μ] : Submodule ℝ ↥(MeasureTheory.Lp ℝ 2 μ)

The Cameron–Martin Hilbert space: the closed first-chaos subspace of centered continuous linear functionals in L²(μ).

Equations

• CameronMartin.Space μ = (↑(StrongDual.toLp μ 2 - MeasureTheory.Lp.constL 2 μ ℝ ∘SL (ContinuousLinearMap.apply ℝ ℝ) (∫ (x : W), x ∂μ))).range.topologicalClosure

noncomputable def CameronMartin.centeredId {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] (μ : MeasureTheory.Measure W) : W → W

The identity random variable centered by its Bochner mean.

Equations

• CameronMartin.centeredId μ = id - fun (x : W) => ∫ (x : W), x ∂μ

theorem CameronMartin.memLp_centeredId {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [CompleteSpace W] [MeasurableSpace W] [BorelSpace W] [SecondCountableTopology W] (μ : MeasureTheory.Measure W) [ProbabilityTheory.IsGaussian μ] : MeasureTheory.MemLp (centeredId μ) 2 μ

The centered identity is square-integrable under a Gaussian measure.

noncomputable def CameronMartin.centeredIdLp {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [CompleteSpace W] [MeasurableSpace W] [BorelSpace W] [SecondCountableTopology W] (μ : MeasureTheory.Measure W) [ProbabilityTheory.IsGaussian μ] : ↥(MeasureTheory.Lp W 2 μ)

The centered identity as an element of L²(μ; W).

Equations

• CameronMartin.centeredIdLp μ = MeasureTheory.MemLp.toLp (CameronMartin.centeredId μ) ⋯

noncomputable def CameronMartin.covarianceMap {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [CompleteSpace W] [MeasurableSpace W] [BorelSpace W] [SecondCountableTopology W] (μ : MeasureTheory.Measure W) [ProbabilityTheory.IsGaussian μ] : ↥(MeasureTheory.Lp ℝ 2 μ) →L[ℝ] W

The covariance map from scalar L²(μ) into the ambient Banach space.

Equations

• CameronMartin.covarianceMap μ = (ContinuousLinearMap.lpPairing μ 2 2 (ContinuousLinearMap.lsmul ℝ ℝ)).flip (CameronMartin.centeredIdLp μ)

noncomputable def CameronMartin.inclusion {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [CompleteSpace W] [MeasurableSpace W] [BorelSpace W] [SecondCountableTopology W] (μ : MeasureTheory.Measure W) [ProbabilityTheory.IsGaussian μ] : ↥(Space μ) →L[ℝ] W

The covariance embedding of the Cameron–Martin space into W.

Equations

• CameronMartin.inclusion μ = (CameronMartin.covarianceMap μ).domRestrict (CameronMartin.Space μ)

instance CameronMartin.instCompleteSpaceSpace {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] [BorelSpace W] (μ : MeasureTheory.Measure W) [ProbabilityTheory.IsGaussian μ] : CompleteSpace ↥(Space μ)

The Cameron–Martin space is complete because it is a closed subspace of L²(μ).

noncomputable def mderiv {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [CompleteSpace W] [MeasurableSpace W] [BorelSpace W] [SecondCountableTopology W] (μ : MeasureTheory.Measure W) [ProbabilityTheory.IsGaussian μ] (F : W → ℝ) (x : W) : ↥(CameronMartin.Space μ)

The Malliavin derivative as the Riesz representative of differentiation along the Cameron–Martin covariance embedding.

Equations

• mderiv μ F x = (InnerProductSpace.toDual ℝ ↥(CameronMartin.Space μ)).symm (fderiv ℝ F x ∘SL CameronMartin.inclusion μ)

structure IsSmoothBounded {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (F : W → ℝ) : Prop

A bounded C¹ Fréchet functional with uniformly bounded derivative.

• contDiff : ContDiff ℝ 1 F
• bounded : ∃ (C : ℝ), ∀ (x : W), |F x| ≤ C
• bounded_fderiv : ∃ (C : ℝ), ∀ (x : W), ‖fderiv ℝ F x‖ ≤ C

theorem IsSmoothBounded.toMalliavin {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] {F : W → ℝ} (hF : IsSmoothBounded F) : Malliavin.IsSmoothBounded F

Convert the independent statement boundary to the library's smoothness predicate.

theorem IsSmoothBounded.continuous_fderiv {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] {F : W → ℝ} (hF : IsSmoothBounded F) : Continuous (fderiv ℝ F)

A smooth bounded functional has a continuous Fréchet derivative.

theorem IsSmoothBounded.memLp {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] [BorelSpace W] {F : W → ℝ} (μ : MeasureTheory.Measure W) [ProbabilityTheory.IsGaussian μ] (hF : IsSmoothBounded F) (p : ENNReal) : MeasureTheory.MemLp F p μ

A smooth bounded functional belongs to every finite or infinite Lᵖ space.

theorem IsSmoothBounded.continuous_mderiv {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [CompleteSpace W] [MeasurableSpace W] [BorelSpace W] [SecondCountableTopology W] {F : W → ℝ} (μ : MeasureTheory.Measure W) [ProbabilityTheory.IsGaussian μ] (hF : IsSmoothBounded F) : Continuous (mderiv μ F)

The Malliavin derivative of a smooth bounded functional is continuous.

theorem IsSmoothBounded.exists_norm_mderiv_le {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [CompleteSpace W] [MeasurableSpace W] [BorelSpace W] [SecondCountableTopology W] {F : W → ℝ} (μ : MeasureTheory.Measure W) [ProbabilityTheory.IsGaussian μ] (hF : IsSmoothBounded F) : ∃ (C : ℝ), ∀ (x : W), ‖mderiv μ F x‖ ≤ C

The norm of the Malliavin derivative is uniformly bounded.

theorem IsSmoothBounded.memLp_mderiv {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [CompleteSpace W] [MeasurableSpace W] [BorelSpace W] [SecondCountableTopology W] {F : W → ℝ} (μ : MeasureTheory.Measure W) [ProbabilityTheory.IsGaussian μ] (hF : IsSmoothBounded F) (p : ENNReal) : MeasureTheory.MemLp (mderiv μ F) p μ

The Malliavin derivative of a smooth bounded functional belongs to Lᵖ for every p.

noncomputable def IsSmoothBounded.toLp {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] [BorelSpace W] {F : W → ℝ} (μ : MeasureTheory.Measure W) [ProbabilityTheory.IsGaussian μ] (hF : IsSmoothBounded F) : ↥(MeasureTheory.Lp ℝ 2 μ)

The L²(μ) equivalence class of a smooth bounded functional.

Equations

• IsSmoothBounded.toLp μ hF = MeasureTheory.MemLp.toLp F ⋯

noncomputable def IsSmoothBounded.mderivLp {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [CompleteSpace W] [MeasurableSpace W] [BorelSpace W] [SecondCountableTopology W] {F : W → ℝ} (μ : MeasureTheory.Measure W) [ProbabilityTheory.IsGaussian μ] (hF : IsSmoothBounded F) : ↥(MeasureTheory.Lp (↥(CameronMartin.Space μ)) 2 μ)

The Malliavin derivative of a smooth bounded functional as an element of L²(μ; H), where H is the Cameron–Martin space.

Equations

• IsSmoothBounded.mderivLp μ hF = MeasureTheory.MemLp.toLp (mderiv μ F) ⋯

theorem integral_inner_mderiv {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [CompleteSpace W] [MeasurableSpace W] [BorelSpace W] [SecondCountableTopology W] (μ : MeasureTheory.Measure W) [ProbabilityTheory.IsGaussian μ] {F : W → ℝ} (hF : IsSmoothBounded F) (h : ↥(CameronMartin.Space μ)) : ∫ (x : W), inner ℝ (mderiv μ F x) h ∂μ = ∫ (x : W), F x * ↑↑↑h x ∂μ

Gaussian integration by parts: the mean directional Malliavin derivative along a Cameron–Martin vector equals pairing against its first-chaos representative.

theorem mderiv_closable {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [CompleteSpace W] [MeasurableSpace W] [BorelSpace W] [SecondCountableTopology W] (μ : MeasureTheory.Measure W) [ProbabilityTheory.IsGaussian μ] (F : ℕ → { F : W → ℝ // IsSmoothBounded F }) {η : ↥(MeasureTheory.Lp (↥(CameronMartin.Space μ)) 2 μ)} (hF : Filter.Tendsto (fun (k : ℕ) => IsSmoothBounded.toLp μ ⋯) Filter.atTop (nhds 0)) (hD : Filter.Tendsto (fun (k : ℕ) => IsSmoothBounded.mderivLp μ ⋯) Filter.atTop (nhds η)) : η = 0