production module

`AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalLocalProgressiveL2`

4 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/GlobalLocalProgressiveL2.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.LocalProgressiveL2

Imported by

AutoSamplingTheory.TechnicalLemmas.StochasticProcessesAutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FiniteDimensionalNormBridgeAutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalCanonicalLocalizerTests.GlobalLocalProgressiveL2

Placeholder scan

0 declaration(s) flagged

Gate status

Compiled

Declarations

structure AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalLocalProgressiveL2.GlobalLocalProgressiveL2Integrand Compiled Not mapped

- A progressive process satisfying Chewi's local square-integrability condition (1.1.10) on every finite horizon. This is the rigorous global domain needed by Proposition 1.1.16.

structure GlobalLocalProgressiveL2Integrand
    {Omega : Type*} {m : MeasurableSpace Omega}
    (filtration : Filtration ℝ≥0 m) (mu : Measure Omega) where
  process : ℝ≥0 → Omega → ℝ
  progressive : IsStronglyProgressive filtration process
  finiteEnergy : ∀ T : ℝ≥0, IsLocallySquareIntegrableOn process mu T

namespace GlobalLocalProgressiveL2Integrand

variable {Omega : Type*} {m : MeasurableSpace Omega}
  {filtration : Filtration ℝ≥0 m} {mu : Measure Omega}

/-- Restrict the global source domain to a finite horizon, recovering the
existing localization input type exactly. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/GlobalLocalProgressiveL2.lean:31published source at 7bcd37294df1

def

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalLocalProgressiveL2.GlobalLocalProgressiveL2Integrand.onHorizon

Compiled Not mapped

- Restrict the global source domain to a finite horizon, recovering the existing localization input type exactly.

def onHorizon (eta : GlobalLocalProgressiveL2Integrand filtration mu) (T : ℝ≥0) :
    LocalProgressiveL2Integrand filtration mu T where
  process := eta.process
  progressive := eta.progressive
  finiteEnergy := eta.finiteEnergy T

@[simp]

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/GlobalLocalProgressiveL2.lean:45published source at 7bcd37294df1

theorem

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalLocalProgressiveL2.GlobalLocalProgressiveL2Integrand.onHorizon_process

Compiled Not mapped

No declaration docstring.

theorem onHorizon_process
    (eta : GlobalLocalProgressiveL2Integrand filtration mu) (T : ℝ≥0) :
    (eta.onHorizon T).process = eta.process := rfl

/-- Source-facing restatement of the implicit global form of (1.1.10). -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/GlobalLocalProgressiveL2.lean:52published source at 7bcd37294df1

theorem

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalLocalProgressiveL2.GlobalLocalProgressiveL2Integrand.chewi_global_condition_1_1_10

Compiled Not mapped

- Source-facing restatement of the implicit global form of (1.1.10).

theorem chewi_global_condition_1_1_10
    (eta : GlobalLocalProgressiveL2Integrand filtration mu) :
    ∀ T : ℝ≥0, IsLocallySquareIntegrableOn eta.process mu T :=
  eta.finiteEnergy

end GlobalLocalProgressiveL2Integrand
end GlobalLocalProgressiveL2
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/GlobalLocalProgressiveL2.lean:57published source at 7bcd37294df1