The closed range of the constructed Itô integral

This packages the natural Itô terminal values as closed subspaces of ambient and centered L²(P), constructs the orthogonal projection onto the centered range, and restates martingale representation as triviality of the corresponding orthogonal complement.

The ambient closed range

noncomputable def Malliavin.naturalItoRange {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] [SecondCountableTopology W] {P : MeasureTheory.Measure W} [ProbabilityTheory.IsGaussian P] {B : NNReal → W → ℝ} (hB : ProbabilityTheory.IsPreBrownianReal B P) (hsm : ∀ (t : NNReal), MeasureTheory.StronglyMeasurable (B t)) {𝓅 : MeasureTheory.Filtration NNReal inst✝} (hnat : 𝓅 = MeasureTheory.Filtration.natural B hsm) : Submodule ℝ ↥(RandomL2 P)

The subspace of terminal L²(P) random variables obtained from the constructed natural Itô integral.

Equations

• Malliavin.naturalItoRange hB hsm hnat = (↑(Malliavin.naturalItoIntegral hB hsm hnat)).range

theorem Malliavin.isClosed_naturalItoRange {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] [SecondCountableTopology W] {P : MeasureTheory.Measure W} [ProbabilityTheory.IsGaussian P] {B : NNReal → W → ℝ} (hB : ProbabilityTheory.IsPreBrownianReal B P) (hsm : ∀ (t : NNReal), MeasureTheory.StronglyMeasurable (B t)) {𝓅 : MeasureTheory.Filtration NNReal inst✝} (hnat : 𝓅 = MeasureTheory.Filtration.natural B hsm) : IsClosed ↑(naturalItoRange hB hsm hnat)

The natural Itô terminal-value subspace is closed in L²(P).

theorem Malliavin.naturalItoRange_le_expectationMap_ker {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] [SecondCountableTopology W] {P : MeasureTheory.Measure W} [ProbabilityTheory.IsGaussian P] {B : NNReal → W → ℝ} (hB : ProbabilityTheory.IsPreBrownianReal B P) (hsm : ∀ (t : NNReal), MeasureTheory.StronglyMeasurable (B t)) {𝓅 : MeasureTheory.Filtration NNReal inst✝} (hnat : 𝓅 = MeasureTheory.Filtration.natural B hsm) : naturalItoRange hB hsm hnat ≤ (↑(CameronMartin.expectationMap P)).ker

Every natural Itô terminal value is centered.

theorem Malliavin.firstChaos_le_naturalItoRange {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] [SecondCountableTopology W] {P : MeasureTheory.Measure W} [ProbabilityTheory.IsGaussian P] {B : NNReal → W → ℝ} (hB : ProbabilityTheory.IsPreBrownianReal B P) (hsm : ∀ (t : NNReal), MeasureTheory.StronglyMeasurable (B t)) {𝓅 : MeasureTheory.Filtration NNReal inst✝} (hnat : 𝓅 = MeasureTheory.Filtration.natural B hsm) : firstChaos hB ≤ naturalItoRange hB hsm hnat

The natural Itô terminal-value subspace contains the full Gaussian first chaos.

The range inside centered L²

noncomputable def Malliavin.centeredNaturalItoRange {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] [SecondCountableTopology W] {P : MeasureTheory.Measure W} [ProbabilityTheory.IsGaussian P] {B : NNReal → W → ℝ} (hB : ProbabilityTheory.IsPreBrownianReal B P) (hsm : ∀ (t : NNReal), MeasureTheory.StronglyMeasurable (B t)) {𝓅 : MeasureTheory.Filtration NNReal inst✝} (hnat : 𝓅 = MeasureTheory.Filtration.natural B hsm) : Submodule ℝ ↥(↑(CameronMartin.expectationMap P)).ker

The same terminal-value range, intrinsically regarded as a subspace of centered L²(P).

Equations

• Malliavin.centeredNaturalItoRange hB hsm hnat = (Malliavin.centeredNaturalItoIntegralIsometry hB hsm hnat).range

theorem Malliavin.isClosed_centeredNaturalItoRange {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] [SecondCountableTopology W] {P : MeasureTheory.Measure W} [ProbabilityTheory.IsGaussian P] {B : NNReal → W → ℝ} (hB : ProbabilityTheory.IsPreBrownianReal B P) (hsm : ∀ (t : NNReal), MeasureTheory.StronglyMeasurable (B t)) {𝓅 : MeasureTheory.Filtration NNReal inst✝} (hnat : 𝓅 = MeasureTheory.Filtration.natural B hsm) : IsClosed ↑(centeredNaturalItoRange hB hsm hnat)

The centered natural Itô range is closed.

theorem Malliavin.mem_centeredNaturalItoRange_iff {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] [SecondCountableTopology W] {P : MeasureTheory.Measure W} [ProbabilityTheory.IsGaussian P] {B : NNReal → W → ℝ} (hB : ProbabilityTheory.IsPreBrownianReal B P) (hsm : ∀ (t : NNReal), MeasureTheory.StronglyMeasurable (B t)) {𝓅 : MeasureTheory.Filtration NNReal inst✝} (hnat : 𝓅 = MeasureTheory.Filtration.natural B hsm) (G : ↥(↑(CameronMartin.expectationMap P)).ker) : G ∈ centeredNaturalItoRange hB hsm hnat ↔ ↑G ∈ naturalItoRange hB hsm hnat

Membership in the intrinsic centered range is equivalent to ambient membership in the natural Itô range.

noncomputable def Malliavin.centeredNaturalItoRangeProjection {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] [SecondCountableTopology W] {P : MeasureTheory.Measure W} [ProbabilityTheory.IsGaussian P] {B : NNReal → W → ℝ} (hB : ProbabilityTheory.IsPreBrownianReal B P) (hsm : ∀ (t : NNReal), MeasureTheory.StronglyMeasurable (B t)) {𝓅 : MeasureTheory.Filtration NNReal inst✝} (hnat : 𝓅 = MeasureTheory.Filtration.natural B hsm) : ↥(↑(CameronMartin.expectationMap P)).ker →L[ℝ] ↥(centeredNaturalItoRange hB hsm hnat)

Orthogonal projection from centered L²(P) onto the closed centered natural Itô range.

Equations

• Malliavin.centeredNaturalItoRangeProjection hB hsm hnat = (Malliavin.centeredNaturalItoRange hB hsm hnat).orthogonalProjectionOnto

noncomputable def Malliavin.centeredNaturalItoRangeEquiv {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] [SecondCountableTopology W] {P : MeasureTheory.Measure W} [ProbabilityTheory.IsGaussian P] {B : NNReal → W → ℝ} (hB : ProbabilityTheory.IsPreBrownianReal B P) (hsm : ∀ (t : NNReal), MeasureTheory.StronglyMeasurable (B t)) {𝓅 : MeasureTheory.Filtration NNReal inst✝} (hnat : 𝓅 = MeasureTheory.Filtration.natural B hsm) : ↥(PredictableProcessL2 𝓅 P) ≃ₗᵢ[ℝ] ↥(centeredNaturalItoRange hB hsm hnat)

The constructed Itô isometry, with codomain restricted to its intrinsic centered range.

Equations

• Malliavin.centeredNaturalItoRangeEquiv hB hsm hnat = (Malliavin.centeredNaturalItoIntegralIsometry hB hsm hnat).equivRange

noncomputable def Malliavin.centeredPartL2 {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] {P : MeasureTheory.Measure W} [ProbabilityTheory.IsGaussian P] (G : ↥(RandomL2 P)) : ↥(↑(CameronMartin.expectationMap P)).ker

The centered part G - E[G], intrinsically regarded as an element of the expectation kernel.

Equations

• Malliavin.centeredPartL2 G = ⟨G - Malliavin.expectationL2 G, ⋯⟩

@[simp]

theorem Malliavin.centeredPartL2_coe {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] {P : MeasureTheory.Measure W} [ProbabilityTheory.IsGaussian P] (G : ↥(RandomL2 P)) : ↑(centeredPartL2 G) = G - expectationL2 G

The ambient value of centeredPartL2 G is G - E[G].

noncomputable def Malliavin.bestNaturalItoIntegrand {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] [SecondCountableTopology W] {P : MeasureTheory.Measure W} [ProbabilityTheory.IsGaussian P] {B : NNReal → W → ℝ} (hB : ProbabilityTheory.IsPreBrownianReal B P) (hsm : ∀ (t : NNReal), MeasureTheory.StronglyMeasurable (B t)) {𝓅 : MeasureTheory.Filtration NNReal inst✝} (hnat : 𝓅 = MeasureTheory.Filtration.natural B hsm) : ↥(↑(CameronMartin.expectationMap P)).ker →L[ℝ] ↥(PredictableProcessL2 𝓅 P)

The canonical best predictable integrand for a centered terminal variable: orthogonally project onto the closed natural Itô range, then invert the Itô isometry on that range.

Equations

• Malliavin.bestNaturalItoIntegrand hB hsm hnat = ↑(↑(Malliavin.centeredNaturalItoRangeEquiv hB hsm hnat)).symm ∘SL Malliavin.centeredNaturalItoRangeProjection hB hsm hnat

noncomputable def Malliavin.bestNaturalItoIntegrandOfRandom {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] [SecondCountableTopology W] {P : MeasureTheory.Measure W} [ProbabilityTheory.IsGaussian P] {B : NNReal → W → ℝ} (hB : ProbabilityTheory.IsPreBrownianReal B P) (hsm : ∀ (t : NNReal), MeasureTheory.StronglyMeasurable (B t)) {𝓅 : MeasureTheory.Filtration NNReal inst✝} (hnat : 𝓅 = MeasureTheory.Filtration.natural B hsm) (G : ↥(RandomL2 P)) : ↥(PredictableProcessL2 𝓅 P)

The canonical best predictable integrand of an arbitrary terminal variable, obtained by first subtracting its expectation.

Equations

• Malliavin.bestNaturalItoIntegrandOfRandom hB hsm hnat G = (Malliavin.bestNaturalItoIntegrand hB hsm hnat) (Malliavin.centeredPartL2 G)

theorem Malliavin.naturalItoIntegral_bestNaturalItoIntegrand {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] [SecondCountableTopology W] {P : MeasureTheory.Measure W} [ProbabilityTheory.IsGaussian P] {B : NNReal → W → ℝ} (hB : ProbabilityTheory.IsPreBrownianReal B P) (hsm : ∀ (t : NNReal), MeasureTheory.StronglyMeasurable (B t)) {𝓅 : MeasureTheory.Filtration NNReal inst✝} (hnat : 𝓅 = MeasureTheory.Filtration.natural B hsm) (G : ↥(↑(CameronMartin.expectationMap P)).ker) : (naturalItoIntegral hB hsm hnat) ((bestNaturalItoIntegrand hB hsm hnat) G) = ↑↑((centeredNaturalItoRangeProjection hB hsm hnat) G)

Integrating the best integrand gives exactly the ambient value of the range projection.

theorem Malliavin.norm_bestNaturalItoIntegrand_le {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] [SecondCountableTopology W] {P : MeasureTheory.Measure W} [ProbabilityTheory.IsGaussian P] {B : NNReal → W → ℝ} (hB : ProbabilityTheory.IsPreBrownianReal B P) (hsm : ∀ (t : NNReal), MeasureTheory.StronglyMeasurable (B t)) {𝓅 : MeasureTheory.Filtration NNReal inst✝} (hnat : 𝓅 = MeasureTheory.Filtration.natural B hsm) (G : ↥(↑(CameronMartin.expectationMap P)).ker) : ‖(bestNaturalItoIntegrand hB hsm hnat) G‖ ≤ ‖G‖

The best-integrand operator is contractive.

@[simp]

theorem Malliavin.bestNaturalItoIntegrand_centeredNaturalItoIntegral {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] [SecondCountableTopology W] {P : MeasureTheory.Measure W} [ProbabilityTheory.IsGaussian P] {B : NNReal → W → ℝ} (hB : ProbabilityTheory.IsPreBrownianReal B P) (hsm : ∀ (t : NNReal), MeasureTheory.StronglyMeasurable (B t)) {𝓅 : MeasureTheory.Filtration NNReal inst✝} (hnat : 𝓅 = MeasureTheory.Filtration.natural B hsm) (U : ↥(PredictableProcessL2 𝓅 P)) : (bestNaturalItoIntegrand hB hsm hnat) ((centeredNaturalItoIntegralIsometry hB hsm hnat) U) = U

On an actual natural Itô terminal value, the best-integrand operator recovers its unique predictable integrand.

noncomputable def Malliavin.centeredWienerIntegral {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] {P : MeasureTheory.Measure W} [ProbabilityTheory.IsGaussian P] {B : NNReal → W → ℝ} (hB : ProbabilityTheory.IsPreBrownianReal B P) (g : ↥(MeasureTheory.Lp ℝ 2 nonnegativeLebesgueMeasure)) : ↥(↑(CameronMartin.expectationMap P)).ker

A deterministic Wiener integral intrinsically regarded as a centered terminal variable.

Equations

• Malliavin.centeredWienerIntegral hB g = ⟨(Malliavin.wienerIntegral hB) g, ⋯⟩

@[simp]

theorem Malliavin.centeredWienerIntegral_coe {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] {P : MeasureTheory.Measure W} [ProbabilityTheory.IsGaussian P] {B : NNReal → W → ℝ} (hB : ProbabilityTheory.IsPreBrownianReal B P) (g : ↥(MeasureTheory.Lp ℝ 2 nonnegativeLebesgueMeasure)) : ↑(centeredWienerIntegral hB g) = (wienerIntegral hB) g

The ambient value of centeredWienerIntegral is the Wiener integral.

theorem Malliavin.bestNaturalItoIntegrand_centeredWienerIntegral {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] [SecondCountableTopology W] {P : MeasureTheory.Measure W} [ProbabilityTheory.IsGaussian P] {B : NNReal → W → ℝ} (hB : ProbabilityTheory.IsPreBrownianReal B P) (hsm : ∀ (t : NNReal), MeasureTheory.StronglyMeasurable (B t)) {𝓅 : MeasureTheory.Filtration NNReal inst✝} (hnat : 𝓅 = MeasureTheory.Filtration.natural B hsm) (g : ↥(MeasureTheory.Lp ℝ 2 nonnegativeLebesgueMeasure)) : (bestNaturalItoIntegrand hB hsm hnat) (centeredWienerIntegral hB g) = (deterministicPredictableEmbedding 𝓅) g

The canonical best integrand of a first-chaos Wiener integral is exactly its deterministic kernel, without any martingale-representation assumption.

theorem Malliavin.sub_centeredNaturalItoRangeProjection_mem_orthogonal {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] [SecondCountableTopology W] {P : MeasureTheory.Measure W} [ProbabilityTheory.IsGaussian P] {B : NNReal → W → ℝ} (hB : ProbabilityTheory.IsPreBrownianReal B P) (hsm : ∀ (t : NNReal), MeasureTheory.StronglyMeasurable (B t)) {𝓅 : MeasureTheory.Filtration NNReal inst✝} (hnat : 𝓅 = MeasureTheory.Filtration.natural B hsm) (G : ↥(↑(CameronMartin.expectationMap P)).ker) : G - ↑((centeredNaturalItoRangeProjection hB hsm hnat) G) ∈ (centeredNaturalItoRange hB hsm hnat)ᗮ

The residual after projecting a centered terminal variable is orthogonal to the entire natural Itô range.

theorem Malliavin.inner_sub_centeredNaturalItoRangeProjection {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] [SecondCountableTopology W] {P : MeasureTheory.Measure W} [ProbabilityTheory.IsGaussian P] {B : NNReal → W → ℝ} (hB : ProbabilityTheory.IsPreBrownianReal B P) (hsm : ∀ (t : NNReal), MeasureTheory.StronglyMeasurable (B t)) {𝓅 : MeasureTheory.Filtration NNReal inst✝} (hnat : 𝓅 = MeasureTheory.Filtration.natural B hsm) (G : ↥(↑(CameronMartin.expectationMap P)).ker) (U : ↥(PredictableProcessL2 𝓅 P)) : inner ℝ (G - ↑((centeredNaturalItoRangeProjection hB hsm hnat) G)) ((centeredNaturalItoIntegralIsometry hB hsm hnat) U) = 0

Equivalently, the residual is orthogonal to the integral of every predictable process.

theorem Malliavin.norm_sub_centeredNaturalItoIntegral_bestNaturalItoIntegrand_le {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] [SecondCountableTopology W] {P : MeasureTheory.Measure W} [ProbabilityTheory.IsGaussian P] {B : NNReal → W → ℝ} (hB : ProbabilityTheory.IsPreBrownianReal B P) (hsm : ∀ (t : NNReal), MeasureTheory.StronglyMeasurable (B t)) {𝓅 : MeasureTheory.Filtration NNReal inst✝} (hnat : 𝓅 = MeasureTheory.Filtration.natural B hsm) (G : ↥(↑(CameronMartin.expectationMap P)).ker) (U : ↥(PredictableProcessL2 𝓅 P)) : ‖G - (centeredNaturalItoIntegralIsometry hB hsm hnat) ((bestNaturalItoIntegrand hB hsm hnat) G)‖ ≤ ‖G - (centeredNaturalItoIntegralIsometry hB hsm hnat) U‖

The best integrand minimizes the centered L² reconstruction error among all predictable integrands.

theorem Malliavin.naturalMartingaleRepresentation_iff_centeredNaturalItoRange_eq_top {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] [SecondCountableTopology W] {P : MeasureTheory.Measure W} [ProbabilityTheory.IsGaussian P] {B : NNReal → W → ℝ} (hB : ProbabilityTheory.IsPreBrownianReal B P) (hsm : ∀ (t : NNReal), MeasureTheory.StronglyMeasurable (B t)) {𝓅 : MeasureTheory.Filtration NNReal inst✝} (hnat : 𝓅 = MeasureTheory.Filtration.natural B hsm) : NaturalMartingaleRepresentation hB hsm hnat ↔ centeredNaturalItoRange hB hsm hnat = ⊤

Martingale representation is equivalent to the centered natural Itô range being the whole centered L²(P) space.

theorem Malliavin.naturalMartingaleRepresentation_iff_centeredNaturalItoRange_orthogonal_eq_bot {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] [SecondCountableTopology W] {P : MeasureTheory.Measure W} [ProbabilityTheory.IsGaussian P] {B : NNReal → W → ℝ} (hB : ProbabilityTheory.IsPreBrownianReal B P) (hsm : ∀ (t : NNReal), MeasureTheory.StronglyMeasurable (B t)) {𝓅 : MeasureTheory.Filtration NNReal inst✝} (hnat : 𝓅 = MeasureTheory.Filtration.natural B hsm) : NaturalMartingaleRepresentation hB hsm hnat ↔ (centeredNaturalItoRange hB hsm hnat)ᗮ = ⊥

Martingale representation holds exactly when no nonzero centered random variable is orthogonal to every natural Itô terminal value.

theorem Malliavin.centeredNaturalItoIntegral_bestNaturalItoIntegrand {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] [SecondCountableTopology W] {P : MeasureTheory.Measure W} [ProbabilityTheory.IsGaussian P] {B : NNReal → W → ℝ} (hB : ProbabilityTheory.IsPreBrownianReal B P) (hsm : ∀ (t : NNReal), MeasureTheory.StronglyMeasurable (B t)) {𝓅 : MeasureTheory.Filtration NNReal inst✝} (hnat : 𝓅 = MeasureTheory.Filtration.natural B hsm) (hMRT : NaturalMartingaleRepresentation hB hsm hnat) (G : ↥(↑(CameronMartin.expectationMap P)).ker) : (centeredNaturalItoIntegralIsometry hB hsm hnat) ((bestNaturalItoIntegrand hB hsm hnat) G) = G

Under martingale representation, the best integrand recovers every centered terminal variable exactly.

theorem Malliavin.naturalMartingaleRepresentation_canonical {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] [SecondCountableTopology W] {P : MeasureTheory.Measure W} [ProbabilityTheory.IsGaussian P] {B : NNReal → W → ℝ} (hB : ProbabilityTheory.IsPreBrownianReal B P) (hsm : ∀ (t : NNReal), MeasureTheory.StronglyMeasurable (B t)) {𝓅 : MeasureTheory.Filtration NNReal inst✝} (hnat : 𝓅 = MeasureTheory.Filtration.natural B hsm) (hMRT : NaturalMartingaleRepresentation hB hsm hnat) (G : ↥(RandomL2 P)) : G = expectationL2 G + (naturalItoIntegral hB hsm hnat) (bestNaturalItoIntegrandOfRandom hB hsm hnat G)

Under martingale representation, the canonical best integrand gives a chosen representation of every terminal variable, rather than merely an existential one.

theorem Malliavin.naturalMartingaleRepresentation_iff_canonical {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] [SecondCountableTopology W] {P : MeasureTheory.Measure W} [ProbabilityTheory.IsGaussian P] {B : NNReal → W → ℝ} (hB : ProbabilityTheory.IsPreBrownianReal B P) (hsm : ∀ (t : NNReal), MeasureTheory.StronglyMeasurable (B t)) {𝓅 : MeasureTheory.Filtration NNReal inst✝} (hnat : 𝓅 = MeasureTheory.Filtration.natural B hsm) : NaturalMartingaleRepresentation hB hsm hnat ↔ ∀ (G : ↥(RandomL2 P)), G = expectationL2 G + (naturalItoIntegral hB hsm hnat) (bestNaturalItoIntegrandOfRandom hB hsm hnat G)

Martingale representation holds exactly when the canonical best-integrand formula reconstructs every terminal variable.

theorem Malliavin.naturalMartingaleRepresentation_iff_bestNaturalItoIntegrand_exact {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] [SecondCountableTopology W] {P : MeasureTheory.Measure W} [ProbabilityTheory.IsGaussian P] {B : NNReal → W → ℝ} (hB : ProbabilityTheory.IsPreBrownianReal B P) (hsm : ∀ (t : NNReal), MeasureTheory.StronglyMeasurable (B t)) {𝓅 : MeasureTheory.Filtration NNReal inst✝} (hnat : 𝓅 = MeasureTheory.Filtration.natural B hsm) : NaturalMartingaleRepresentation hB hsm hnat ↔ ∀ (G : ↥(↑(CameronMartin.expectationMap P)).ker), (centeredNaturalItoIntegralIsometry hB hsm hnat) ((bestNaturalItoIntegrand hB hsm hnat) G) = G

Martingale representation is also equivalent to the canonical best-integrand operator being an exact right inverse on every centered terminal variable.