production module

`AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Truncation`

8 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Truncation.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CoefficientTruncationAutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2

Imported by

AutoSamplingTheory.TechnicalLemmas.StochasticProcessesAutoSamplingTheory.TechnicalLemmas.StochasticProcesses.LaggedDyadicApproximationTests.ProgressiveL2Truncation

Placeholder scan

0 declaration(s) flagged

Gate status

Compiled

Declarations

def AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Truncation.clipProcess Compiled Not mapped

- Pointwise clipping of a stochastic process.

def clipProcess (n : ℕ) (eta : ℝ≥0 → Omega → ℝ) : ℝ≥0 → Omega → ℝ :=
  fun t omega => clipNat n (eta t omega)

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Truncation.lean:26published source at 7bcd37294df1

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Truncation.clipProcess_stronglyProgressive Compiled Not mapped

No declaration docstring.

theorem clipProcess_stronglyProgressive
    (eta : ProgressiveL2Integrand filtration mu T) (n : ℕ) :
    IsStronglyProgressive filtration (clipProcess n eta.process) := by
  intro t
  exact stronglyMeasurable_clipNat (eta.progressive t) n

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Truncation.lean:29published source at 7bcd37294df1

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Truncation.processFunction_clipProcess Compiled Not mapped

No declaration docstring.

theorem processFunction_clipProcess
    (eta : ℝ≥0 → Omega → ℝ) (n : ℕ) :
    processFunction (clipProcess n eta) =
      fun z => clipNat n (processFunction eta z) :=
  rfl

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Truncation.lean:35published source at 7bcd37294df1

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Truncation.clipProcess_memLp Compiled Not mapped

No declaration docstring.

theorem clipProcess_memLp
    (eta : ProgressiveL2Integrand filtration mu T) (n : ℕ) :
    MemLp (processFunction (clipProcess n eta.process)) 2
      (processTimeMeasure mu T) := by
  rw [processFunction_clipProcess]
  exact clipNat_memLp eta.memLp n

/-- Clipping as an endomorphism of the progressive `L2` integrand domain. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Truncation.lean:41published source at 7bcd37294df1

def AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Truncation.clipped Compiled Compiled

- Clipping as an endomorphism of the progressive `L2` integrand domain.

noncomputable def clipped
    (eta : ProgressiveL2Integrand filtration mu T) (n : ℕ) :
    ProgressiveL2Integrand filtration mu T where
  process := clipProcess n eta.process
  progressive := clipProcess_stronglyProgressive eta n
  memLp := clipProcess_memLp eta n

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Truncation.lean:49published source at 7bcd37294df1Open detailed card

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Truncation.clipped_process Compiled Not mapped

No declaration docstring.

@[simp] theorem clipped_process
    (eta : ProgressiveL2Integrand filtration mu T) (n : ℕ) :
    (clipped eta n).process = clipProcess n eta.process :=
  rfl

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Truncation.lean:56published source at 7bcd37294df1

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Truncation.clipped_abs_le Compiled Not mapped

No declaration docstring.

theorem clipped_abs_le
    (eta : ProgressiveL2Integrand filtration mu T) (n : ℕ)
    (t : ℝ≥0) (omega : Omega) :
    |(clipped eta n).process t omega| ≤ (n : ℝ) :=
  abs_clipNat_le n _

/-- Bounded progressive truncations converge to the original integrand in
the actual product-space `Lp` object. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Truncation.lean:61published source at 7bcd37294df1

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Truncation.tendsto_clipped_toLp Compiled Not mapped

- Bounded progressive truncations converge to the original integrand in the actual product-space `Lp` object.

theorem tendsto_clipped_toLp
    (eta : ProgressiveL2Integrand filtration mu T) :
    Tendsto (fun n => (clipped eta n).toLp) atTop (𝓝 eta.toLp) := by
  simpa [ProgressiveL2Integrand.toLp, clipped, processFunction_clipProcess] using
    (tendsto_clipNat_toLp eta.memLp)

end ProgressiveL2Truncation
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Truncation.lean:69published source at 7bcd37294df1Open detailed card