Malliavin calculus through the Clark--Ocone formula

This statement gives explicit Mathlib-only meanings to the Cameron--Martin space, the smooth Malliavin derivative, its graph closure, predictable projection, and the natural predictable process space. The theorem supplies the time realization and Brownian Itô isometry and states martingale representation together with the Clark--Ocone identity on the closed graph. The explicit boundary definitions support independent statement auditing; named bridges transfer their witnesses to the shared library API.

noncomputable def PalomarClarkOcone.nonnegativeLebesgueMeasure : MeasureTheory.Measure NNReal

Lebesgue measure on nonnegative time.

Equations

• PalomarClarkOcone.nonnegativeLebesgueMeasure = MeasureTheory.Measure.comap NNReal.toReal MeasureTheory.volume

@[reducible, inline]

abbrev PalomarClarkOcone.RandomL2 {W : Type u} [MeasurableSpace W] (P : MeasureTheory.Measure W) : AddSubgroup (W →ₘ[P] ℝ)

Square-integrable real random variables.

Equations

• PalomarClarkOcone.RandomL2 P = MeasureTheory.Lp ℝ 2 P

@[reducible, inline]

noncomputable abbrev PalomarClarkOcone.TimeProcessL2 {W : Type u} [MeasurableSpace W] (P : MeasureTheory.Measure W) : AddSubgroup (NNReal × W →ₘ[nonnegativeLebesgueMeasure.prod P] ℝ)

Square-integrable real processes on time times sample space.

Equations

• PalomarClarkOcone.TimeProcessL2 P = MeasureTheory.Lp ℝ 2 (PalomarClarkOcone.nonnegativeLebesgueMeasure.prod P)

@[reducible, inline]

noncomputable abbrev PalomarClarkOcone.PredictableProcessL2 {W : Type u} [MeasurableSpace W] (filtration : MeasureTheory.Filtration NNReal inst✝) (P : MeasureTheory.Measure W) : Submodule ℝ ↥(MeasureTheory.Lp ℝ 2 (nonnegativeLebesgueMeasure.prod P))

Predictable square-integrable processes.

Equations

• PalomarClarkOcone.PredictableProcessL2 filtration P = MeasureTheory.lpMeas ℝ ℝ filtration.predictable 2 (PalomarClarkOcone.nonnegativeLebesgueMeasure.prod P)

@[reducible, inline]

abbrev PalomarClarkOcone.processMeasurableSpace {W : Type u} (B : NNReal → W → ℝ) : MeasurableSpace W

The measurable space generated by a process's coordinates.

Equations

• PalomarClarkOcone.processMeasurableSpace B = ⨆ (t : NNReal), MeasurableSpace.comap (B t) (borel ℝ)

def PalomarClarkOcone.IsWienerGenerated {W : Type u} [MeasurableSpace W] (B : NNReal → W → ℝ) : Prop

The process coordinates generate the ambient measurable space.

Equations

• PalomarClarkOcone.IsWienerGenerated B = (PalomarClarkOcone.processMeasurableSpace B = inst✝)

noncomputable def PalomarClarkOcone.expectationL2 {W : Type u} [MeasurableSpace W] {P : MeasureTheory.Measure W} [MeasureTheory.IsFiniteMeasure P] (G : ↥(RandomL2 P)) : ↥(RandomL2 P)

The constant L² representative of a random variable's expectation.

Equations

• PalomarClarkOcone.expectationL2 G = (MeasureTheory.Lp.const 2 P) (∫ (w : W), ↑↑G w ∂P)

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

The Cameron--Martin Hilbert space.

Equations

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

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

The identity random variable centered by its Bochner mean.

Equations

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

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

The centered identity is square-integrable.

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

The centered identity in L²(P; W).

Equations

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

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

The Gaussian covariance map.

Equations

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

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

The covariance embedding of Cameron--Martin directions into W.

Equations

• PalomarClarkOcone.CameronMartin.inclusion P = (PalomarClarkOcone.CameronMartin.covarianceMap P).domRestrict (PalomarClarkOcone.CameronMartin.Space P)

noncomputable def PalomarClarkOcone.CameronMartin.ofDual {W : Type u} [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] [BorelSpace W] (P : MeasureTheory.Measure W) [ProbabilityTheory.IsGaussian P] : StrongDual ℝ W →L[ℝ] ↥(Space P)

A continuous linear functional as its centered Cameron--Martin class.

Equations

• One or more equations did not get rendered due to their size.

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

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

The smooth Malliavin derivative in Cameron--Martin directions.

Equations

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

noncomputable def PalomarClarkOcone.smulLp {W E : Type u} [MeasurableSpace W] [NormedAddCommGroup E] [NormedSpace ℝ E] {P : MeasureTheory.Measure W} (h : E) : ↥(RandomL2 P) →L[ℝ] ↥(MeasureTheory.Lp E 2 P)

The rank-one H-valued random variable w ↦ G(w)h.

Equations

• PalomarClarkOcone.smulLp h = ContinuousLinearMap.compLpL 2 P (ContinuousLinearMap.toSpanSingleton ℝ h)

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

Bounded C¹ functionals 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 PalomarClarkOcone.IsSmoothBounded.toMalliavin {W : Type u} [NormedAddCommGroup W] [NormedSpace ℝ W] {F : W → ℝ} (hF : IsSmoothBounded F) : Malliavin.IsSmoothBounded F

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

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

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

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

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

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

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

A smooth functional as a scalar L² class.

Equations

• PalomarClarkOcone.IsSmoothBounded.toLp P hF = MeasureTheory.MemLp.toLp F ⋯

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

The smooth Malliavin derivative as an L²(P; H) class.

Equations

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

def PalomarClarkOcone.InGraphClosure {W : Type u} [NormedAddCommGroup W] [NormedSpace ℝ W] [CompleteSpace W] [MeasurableSpace W] [BorelSpace W] [SecondCountableTopology W] (P : MeasureTheory.Measure W) [ProbabilityTheory.IsGaussian P] (F : ↥(MeasureTheory.Lp ℝ 2 P)) (η : ↥(MeasureTheory.Lp (↥(CameronMartin.Space P)) 2 P)) : Prop

(F, η) belongs to the closure of the smooth Malliavin graph.

Equations

• One or more equations did not get rendered due to their size.

theorem PalomarClarkOcone.InGraphClosure.toMalliavin {W : Type u} [NormedAddCommGroup W] [NormedSpace ℝ W] [CompleteSpace W] [MeasurableSpace W] [BorelSpace W] [SecondCountableTopology W] {P : MeasureTheory.Measure W} [ProbabilityTheory.IsGaussian P] {F : ↥(MeasureTheory.Lp ℝ 2 P)} {η : ↥(MeasureTheory.Lp (↥(CameronMartin.Space P)) 2 P)} (h : InGraphClosure P F η) : Malliavin.InGraphClosure P F η

Transfer the independently stated graph closure to the library graph closure.

theorem PalomarClarkOcone.predictable_le_prod {W : Type u} [MeasurableSpace W] (filtration : MeasureTheory.Filtration NNReal inst✝) : filtration.predictable ≤ inferInstance

The predictable sigma-algebra lies below the ambient product sigma-algebra.

noncomputable def PalomarClarkOcone.predictableProjection {W : Type u} [MeasurableSpace W] {P : MeasureTheory.Measure W} (filtration : MeasureTheory.Filtration NNReal inst✝) : ↥(TimeProcessL2 P) →L[ℝ] ↥(PredictableProcessL2 filtration P)

Orthogonal projection onto predictable processes.

Equations

• PalomarClarkOcone.predictableProjection filtration = MeasureTheory.condExpL2 ℝ ℝ ⋯

theorem PalomarClarkOcone.generated_clark_ocone {W : Type u} [NormedAddCommGroup W] [NormedSpace ℝ W] [CompleteSpace W] [MeasurableSpace W] [BorelSpace W] [SecondCountableTopology W] {P : MeasureTheory.Measure W} [ProbabilityTheory.IsGaussian P] {B : NNReal → W → ℝ} (hB : ProbabilityTheory.IsPreBrownianReal B P) (coordinate : NNReal → StrongDual ℝ W) (coordinate_apply : ∀ (t : NNReal) (w : W), B t w = (coordinate t) w) (generated : IsWienerGenerated B) (hsm : ∀ (t : NNReal), MeasureTheory.StronglyMeasurable (B t)) {filtration : MeasureTheory.Filtration NNReal inst✝} (hnat : filtration = MeasureTheory.Filtration.natural B hsm) : ∃ (timeDerivative : ↥(MeasureTheory.Lp (↥(CameronMartin.Space P)) 2 P) →ₗᵢ[ℝ] ↥(TimeProcessL2 P)) (itoIntegral : ↥(PredictableProcessL2 filtration P) →L[ℝ] ↥(RandomL2 P)), (∀ (h : ↥(CameronMartin.Space P)), (∀ (t : NNReal), inner ℝ h ((CameronMartin.ofDual P) (coordinate t)) = 0) → h = 0) ∧ (∀ (t : NNReal) (G : ↥(RandomL2 P)), ↑↑(timeDerivative ((smulLp ((CameronMartin.ofDual P) (coordinate t))) G)) =ᵐ[nonnegativeLebesgueMeasure.prod P] fun (p : NNReal × W) => (Set.Ioc 0 t).indicator 1 p.1 * ↑↑G p.2) ∧ (∀ (U : ↥(PredictableProcessL2 filtration P)), ‖itoIntegral U‖ = ‖U‖) ∧ (∀ (U : ↥(PredictableProcessL2 filtration P)), ∫ (w : W), ↑↑(itoIntegral U) w ∂P = 0) ∧ (∀ {a b : NNReal}, a ≤ b → ∀ (Z : ↥(MeasureTheory.lpMeas ℝ ℝ (↑filtration a) 2 P)), ∃ (U : ↥(PredictableProcessL2 filtration P)), (↑↑↑U =ᵐ[nonnegativeLebesgueMeasure.prod P] fun (p : NNReal × W) => (Set.Ioc a b).indicator 1 p.1 * ↑↑↑Z p.2) ∧ ↑↑(itoIntegral U) =ᵐ[P] fun (w : W) => ↑↑↑Z w * (B b w - B a w)) ∧ (∀ (G : ↥(RandomL2 P)), ∃ (U : ↥(PredictableProcessL2 filtration P)), G = expectationL2 G + itoIntegral U) ∧ ∀ {F : ↥(RandomL2 P)} {η : ↥(MeasureTheory.Lp (↥(CameronMartin.Space P)) 2 P)}, InGraphClosure P F η → ∃ (G : NNReal × W → ℝ), MeasureTheory.StronglyMeasurable G ∧ ↑↑↑((predictableProjection filtration) (timeDerivative η)) =ᵐ[nonnegativeLebesgueMeasure.prod P] G ∧ (∀ᵐ (t : NNReal) ∂nonnegativeLebesgueMeasure, 0 < t → (fun (w : W) => G (t, w)) =ᵐ[P] P[fun (w : W) => ↑↑(timeDerivative η) (t, w) | ↑filtration t]) ∧ F = expectationL2 F + itoIntegral ((predictableProjection filtration) (timeDerivative η))

Generated-space martingale representation and textbook Clark--Ocone. For a generating pre-Brownian process with continuous linear coordinates on a separable real Gaussian Banach space, using its natural filtration, there are a time realization of the closed Malliavin derivative and a Brownian Itô isometry such that every terminal L² variable has a stochastic-integral representation. For every pair in the closed Malliavin graph, the predictable projection of the derivative has a representative whose time sections are the conditional expectations for almost every positive time in the Clark--Ocone identity. The Brownian coordinate directions are total in the Cameron--Martin space, so the displayed generator law determines the continuous time realization.