Samplinglib
Lean gate passed 2026-08-19T06:04:36.257124+00:00 · 77184245109a
production module

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoL2

13 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ElementaryItoL2.lean.

Imports
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoEmbeddingAutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoIsometryMathlib.MeasureTheory.Function.L2Space external
Imported by
AutoSamplingTheory.TechnicalLemmas.StochasticProcessesAutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CoefficientTruncationAutoSamplingTheory.TechnicalLemmas.StochasticProcesses.DyadicElementaryRefinementAutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoProcessAutoSamplingTheory.TechnicalLemmas.StochasticProcesses.RandomStoppingL2ConvergenceTests.ElementaryItoL2
Placeholder scan
0 declaration(s) flagged
Gate status
Compiled

Declarations

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoL2.norm_sq_toLp_eq_integral_sq Compiled Not mapped

- The square of the `L2` norm of a real representative is its second moment.

theorem norm_sq_toLp_eq_integral_sq {f : Omega → ℝ} (hf : MemLp f 2 mu) :
    ‖hf.toLp f‖ ^ 2 = ∫ omega, f omega ^ 2 ∂mu := by
  rw [← real_inner_self_eq_norm_sq, L2.inner_def]
  apply integral_congr_ae
  filter_upwards [hf.coeFn_toLp] with omega homega
  rw [homega]
  simp [pow_two]

/-- The finite elementary stochastic sum is square integrable. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ElementaryItoL2.lean:30published source at 77184245109a

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoL2.elementaryItoIntegral_memLp_two Compiled Not mapped

- The finite elementary stochastic sum is square integrable.

theorem elementaryItoIntegral_memLp_two
    (eta : ElementaryAdaptedProcess filtration n)
    (hB : IsBrownianMotionWithFiltration B filtration mu) (T : ℝ≥0) :
    MemLp (elementaryItoIntegral eta B T) 2 mu := by
  change MemLp (fun omega => ∑ i, weightedIncrement eta B T i omega) 2 mu
  exact memLp_finsetSum Finset.univ fun i _ => weightedIncrement_memLp_two eta hB T i

/-- The elementary terminal Ito integral as an actual element of `L2(mu)`. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ElementaryItoL2.lean:39published source at 77184245109a

def AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoL2.elementaryItoTerminalToLp Compiled Not mapped

- The elementary terminal Ito integral as an actual element of `L2(mu)`.

noncomputable def elementaryItoTerminalToLp
    (eta : ElementaryAdaptedProcess filtration n)
    (hB : IsBrownianMotionWithFiltration B filtration mu) (T : ℝ≥0) :
    Lp ℝ 2 mu :=
  (elementaryItoIntegral_memLp_two eta hB T).toLp
    (elementaryItoIntegral eta B T)

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ElementaryItoL2.lean:47published source at 77184245109a

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoL2.norm_sq_elementaryItoTerminalToLp Compiled Not mapped

No declaration docstring.

theorem norm_sq_elementaryItoTerminalToLp
    (eta : ElementaryAdaptedProcess filtration n)
    (hB : IsBrownianMotionWithFiltration B filtration mu) (T : ℝ≥0) :
    ‖elementaryItoTerminalToLp eta hB T‖ ^ 2 =
      ∫ omega, elementaryItoIntegral eta B T omega ^ 2 ∂mu :=
  norm_sq_toLp_eq_integral_sq (elementaryItoIntegral_memLp_two eta hB T)

/-- The elementary integrand as a product-space `L2` element in the Brownian
probability environment. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ElementaryItoL2.lean:54published source at 77184245109a

def AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoL2.elementaryProcessToLp Compiled Not mapped

- The elementary integrand as a product-space `L2` element in the Brownian probability environment.

noncomputable def elementaryProcessToLp
    (eta : ElementaryAdaptedProcess filtration n)
    (hB : IsBrownianMotionWithFiltration B filtration mu) (T : ℝ≥0) :
    Lp ℝ 2 (processTimeMeasure mu T) := by
  let _ : IsProbabilityMeasure mu := hB.isProbabilityMeasure
  exact (toProgressiveL2 eta mu T).toLp

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ElementaryItoL2.lean:63published source at 77184245109a

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoL2.ofReal_norm_sq_elementaryProcessToLp_eq_energy Compiled Not mapped

No declaration docstring.

private theorem ofReal_norm_sq_elementaryProcessToLp_eq_energy
    (eta : ElementaryAdaptedProcess filtration n)
    (hB : IsBrownianMotionWithFiltration B filtration mu) (T : ℝ≥0) :
    ENNReal.ofReal (‖elementaryProcessToLp eta hB T‖ ^ 2) =
      processL2Energy eta.value mu T := by
  let _ : IsProbabilityMeasure mu := hB.isProbabilityMeasure
  unfold elementaryProcessToLp
  dsimp only
  have hnorm := norm_sq_toLp_eq_integral_sq (toProgressiveL2 eta mu T).memLp
  change ‖(toProgressiveL2 eta mu T).toLp‖ ^ 2 =
    ∫ z, processFunction (toProgressiveL2 eta mu T).process z ^ 2
      ∂(processTimeMeasure mu T) at hnorm
  rw [hnorm]
  simp only [toProgressiveL2_process]
  have henergy := ofReal_integral_eq_lintegral_ofReal
    (value_memLp_two eta mu T).integrable_sq
    (ae_of_all (processTimeMeasure mu T) fun _ => sq_nonneg _)
  simpa [processL2Energy, processFunction] using henergy

/-- The elementary terminal map is an isometry between the product-space
integrand `L2` norm and the terminal random-variable `L2` norm. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ElementaryItoL2.lean:70published source at 77184245109a

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoL2.norm_elementaryItoTerminalToLp Compiled Not mapped

- The elementary terminal map is an isometry between the product-space integrand `L2` norm and the terminal random-variable `L2` norm.

theorem norm_elementaryItoTerminalToLp
    (eta : ElementaryAdaptedProcess filtration n)
    (hB : IsBrownianMotionWithFiltration B filtration mu) (T : ℝ≥0) :
    ‖elementaryItoTerminalToLp eta hB T‖ =
      ‖elementaryProcessToLp eta hB T‖ := by
  have hterminal : ENNReal.ofReal (‖elementaryItoTerminalToLp eta hB T‖ ^ 2) =
      processL2Energy eta.value mu T := by
    rw [norm_sq_elementaryItoTerminalToLp eta hB T]
    exact chewi_display_1_1_6 eta hB T
  have hprocess := ofReal_norm_sq_elementaryProcessToLp_eq_energy eta hB T
  have hsquares : ‖elementaryItoTerminalToLp eta hB T‖ ^ 2 =
      ‖elementaryProcessToLp eta hB T‖ ^ 2 :=
    (ENNReal.ofReal_eq_ofReal_iff (sq_nonneg _) (sq_nonneg _)).mp
      (hterminal.trans hprocess.symm)
  nlinarith [norm_nonneg (elementaryItoTerminalToLp eta hB T),
    norm_nonneg (elementaryProcessToLp eta hB T)]

/-- On a fixed grid, the terminal `L2` representative respects addition. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ElementaryItoL2.lean:91published source at 77184245109aOpen detailed card

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoL2.elementaryItoTerminalToLp_add Compiled Not mapped

- On a fixed grid, the terminal `L2` representative respects addition.

theorem elementaryItoTerminalToLp_add
    (eta xi : ElementaryAdaptedProcess filtration n)
    (hgrid : eta.times = xi.times)
    (hB : IsBrownianMotionWithFiltration B filtration mu) (T : ℝ≥0) :
    elementaryItoTerminalToLp (add eta xi hgrid) hB T =
      elementaryItoTerminalToLp eta hB T + elementaryItoTerminalToLp xi hB T := by
  apply Lp.ext
  simp only [elementaryItoTerminalToLp]
  filter_upwards [
    (elementaryItoIntegral_memLp_two (add eta xi hgrid) hB T).coeFn_toLp,
    Lp.coeFn_add
      ((elementaryItoIntegral_memLp_two eta hB T).toLp
        (elementaryItoIntegral eta B T))
      ((elementaryItoIntegral_memLp_two xi hB T).toLp
        (elementaryItoIntegral xi B T)),
    (elementaryItoIntegral_memLp_two eta hB T).coeFn_toLp,
    (elementaryItoIntegral_memLp_two xi hB T).coeFn_toLp] with omega hsum hadd heta hxi
  rw [hsum, hadd]
  simp only [Pi.add_apply]
  rw [heta, hxi]
  exact elementaryItoIntegral_add eta xi hgrid B T omega

/-- The Brownian-environment product-space representatives respect same-grid
addition. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ElementaryItoL2.lean:109published source at 77184245109a

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoL2.elementaryProcessToLp_add Compiled Not mapped

- The Brownian-environment product-space representatives respect same-grid addition.

theorem elementaryProcessToLp_add
    (eta xi : ElementaryAdaptedProcess filtration n)
    (hgrid : eta.times = xi.times)
    (hB : IsBrownianMotionWithFiltration B filtration mu) (T : ℝ≥0) :
    elementaryProcessToLp (add eta xi hgrid) hB T =
      elementaryProcessToLp eta hB T + elementaryProcessToLp xi hB T := by
  let _ : IsProbabilityMeasure mu := hB.isProbabilityMeasure
  unfold elementaryProcessToLp
  dsimp only
  exact toLp_add eta xi hgrid mu T

/-- On a common grid, the elementary terminal map preserves the real Hilbert
inner product, not only norms. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ElementaryItoL2.lean:133published source at 77184245109a

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoL2.inner_elementaryItoTerminalToLp Compiled Not mapped

- On a common grid, the elementary terminal map preserves the real Hilbert inner product, not only norms.

theorem inner_elementaryItoTerminalToLp
    (eta xi : ElementaryAdaptedProcess filtration n)
    (hgrid : eta.times = xi.times)
    (hB : IsBrownianMotionWithFiltration B filtration mu) (T : ℝ≥0) :
    ⟪elementaryItoTerminalToLp eta hB T,
        elementaryItoTerminalToLp xi hB T⟫_ℝ =
      ⟪elementaryProcessToLp eta hB T,
        elementaryProcessToLp xi hB T⟫_ℝ := by
  rw [real_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two,
    real_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two,
    ← elementaryItoTerminalToLp_add eta xi hgrid hB T,
    ← elementaryProcessToLp_add eta xi hgrid hB T,
    norm_elementaryItoTerminalToLp (add eta xi hgrid) hB T,
    norm_elementaryItoTerminalToLp eta hB T,
    norm_elementaryItoTerminalToLp xi hB T]

/-- On a fixed grid, the terminal `L2` representative respects subtraction. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ElementaryItoL2.lean:146published source at 77184245109aOpen detailed card

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoL2.elementaryItoTerminalToLp_sub Compiled Not mapped

- On a fixed grid, the terminal `L2` representative respects subtraction.

theorem elementaryItoTerminalToLp_sub
    (eta xi : ElementaryAdaptedProcess filtration n)
    (hgrid : eta.times = xi.times)
    (hB : IsBrownianMotionWithFiltration B filtration mu) (T : ℝ≥0) :
    elementaryItoTerminalToLp (sub eta xi hgrid) hB T =
      elementaryItoTerminalToLp eta hB T - elementaryItoTerminalToLp xi hB T := by
  apply Lp.ext
  simp only [elementaryItoTerminalToLp]
  filter_upwards [
    (elementaryItoIntegral_memLp_two (sub eta xi hgrid) hB T).coeFn_toLp,
    Lp.coeFn_sub
      ((elementaryItoIntegral_memLp_two eta hB T).toLp
        (elementaryItoIntegral eta B T))
      ((elementaryItoIntegral_memLp_two xi hB T).toLp
        (elementaryItoIntegral xi B T)),
    (elementaryItoIntegral_memLp_two eta hB T).coeFn_toLp,
    (elementaryItoIntegral_memLp_two xi hB T).coeFn_toLp] with omega hsub hdiff heta hxi
  rw [hsub, hdiff]
  simp only [Pi.sub_apply]
  rw [heta, hxi]
  exact elementaryItoIntegral_sub eta xi hgrid B T omega

/-- The Brownian-environment product-space representatives respect same-grid
subtraction. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ElementaryItoL2.lean:163published source at 77184245109a

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoL2.elementaryProcessToLp_sub Compiled Not mapped

- The Brownian-environment product-space representatives respect same-grid subtraction.

theorem elementaryProcessToLp_sub
    (eta xi : ElementaryAdaptedProcess filtration n)
    (hgrid : eta.times = xi.times)
    (hB : IsBrownianMotionWithFiltration B filtration mu) (T : ℝ≥0) :
    elementaryProcessToLp (sub eta xi hgrid) hB T =
      elementaryProcessToLp eta hB T - elementaryProcessToLp xi hB T := by
  let _ : IsProbabilityMeasure mu := hB.isProbabilityMeasure
  unfold elementaryProcessToLp
  dsimp only
  exact toLp_sub eta xi hgrid mu T

/-- Same-grid differences satisfy the exact distance form of the elementary
Ito isometry. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ElementaryItoL2.lean:187published source at 77184245109a

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoL2.norm_elementaryItoTerminalToLp_sub Compiled Not mapped

- Same-grid differences satisfy the exact distance form of the elementary Ito isometry.

theorem norm_elementaryItoTerminalToLp_sub
    (eta xi : ElementaryAdaptedProcess filtration n)
    (hgrid : eta.times = xi.times)
    (hB : IsBrownianMotionWithFiltration B filtration mu) (T : ℝ≥0) :
    ‖elementaryItoTerminalToLp eta hB T - elementaryItoTerminalToLp xi hB T‖ =
      ‖elementaryProcessToLp eta hB T - elementaryProcessToLp xi hB T‖ := by
  rw [← elementaryItoTerminalToLp_sub eta xi hgrid hB T,
    ← elementaryProcessToLp_sub eta xi hgrid hB T]
  exact norm_elementaryItoTerminalToLp (sub eta xi hgrid) hB T

end ElementaryItoL2
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ElementaryItoL2.lean:200published source at 77184245109a