Documentation

LeanPool.Malliavin.Malliavin.BrownianChaos

Brownian homogeneous chaoses from iterated Itô integrals #

The ordered-box construction gives canonical Brownian multiple-integral operators. This file defines their closed homogeneous ranges and proves that every positive range lies in the closed range of the natural Itô integral.

source
theorem Malliavin.BrownianIteratedConstruction.simplexIntegral_mem_naturalItoRange_succ {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) {n : ℕ} (f : ↥(IteratedIntegralConstruction.SimplexKernel (n + 1))) :
(simplexIntegral hB (n + 1)) f ∈ naturalItoRange hB hsm hnat

Every completed positive-order simplex integral is a natural Itô terminal value.

source
theorem Malliavin.BrownianIteratedConstruction.positiveIntegralCLM_mem_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) (n : ℕ) (f : ↥(IteratedKernel (n + 1))) :
(positiveIntegralCLM hB n) f ∈ naturalItoRange hB hsm hnat

Every output of the canonical positive-order Brownian operator is a natural Itô terminal value.

source
noncomputable def Malliavin.BrownianIteratedConstruction.brownianMultipleIntegralRange {W : Type u_1} [MeasurableSpace W] {P : MeasureTheory.Measure W} {B : NNReal → W → ℝ} (hB : ProbabilityTheory.IsPreBrownianReal B P) (n : ℕ) :
Submodule ℝ ↥(RandomL2 P)

The unclosed range of the canonical Brownian order-n multiple-integral operator.

Equations
Instances For
    source
    noncomputable def Malliavin.BrownianIteratedConstruction.brownianHomogeneousChaos {W : Type u_1} [MeasurableSpace W] {P : MeasureTheory.Measure W} {B : NNReal → W → ℝ} (hB : ProbabilityTheory.IsPreBrownianReal B P) (n : ℕ) :
    ClosedSubmodule ℝ ↥(RandomL2 P)

    The canonical Brownian nth homogeneous subspace.

    Equations
    Instances For
      source
      theorem Malliavin.BrownianIteratedConstruction.integralCLM_mem_brownianHomogeneousChaos {W : Type u_1} [MeasurableSpace W] {P : MeasureTheory.Measure W} {B : NNReal → W → ℝ} (hB : ProbabilityTheory.IsPreBrownianReal B P) (n : ℕ) (f : ↥(IteratedKernel n)) :
      (integralCLM hB n) f ∈ brownianHomogeneousChaos hB n

      Every output of the canonical order-n operator belongs to its Brownian homogeneous chaos.

      source
      theorem Malliavin.BrownianIteratedConstruction.brownianMultipleIntegralRange_isOrtho {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)) {m n : ℕ} (hmn : m ≠ n) :
      brownianMultipleIntegralRange hB m ⟂ brownianMultipleIntegralRange hB n

      The unclosed Brownian multiple-integral ranges of distinct orders are orthogonal.

      source
      theorem Malliavin.BrownianIteratedConstruction.brownianHomogeneousChaos_isOrtho {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)) {m n : ℕ} (hmn : m ≠ n) :
      ↑(brownianHomogeneousChaos hB m) ⟂ ↑(brownianHomogeneousChaos hB n)

      Distinct closed Brownian homogeneous chaoses remain orthogonal.

      source
      theorem Malliavin.BrownianIteratedConstruction.brownianHomogeneousChaos_zero_le_centeredPartCLM_ker {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) :
      ↑(brownianHomogeneousChaos hB 0) ≤ (↑centeredPartCLM).ker

      The zeroth Brownian homogeneous chaos is killed by the centering operator.

      source
      theorem Malliavin.BrownianIteratedConstruction.brownianHomogeneousChaos_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) (n : ℕ) (hn : 0 < n) :
      ↑(brownianHomogeneousChaos hB n) ≤ naturalItoRange hB hsm hnat

      Every positive Brownian homogeneous chaos lies in the natural Itô range.