Samplinglib
Lean gate passed 2026-08-19T06:32:39.895922+00:00 · 7bcd37294df1
production module

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Algebra

21 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Algebra.lean.

Imports
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2
Imported by
AutoSamplingTheory.TechnicalLemmas.StochasticProcessesAutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ItoIntegralProcessCongruenceAutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ItoTerminalCompletionAutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2HorizonExtensionAutoSamplingTheory.TechnicalLemmas.StochasticProcesses.RandomStoppingProcessConsistencyTests.ProgressiveL2Tests.ProgressiveL2Algebra
Placeholder scan
0 declaration(s) flagged
Gate status
Compiled

Declarations

def AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Algebra.zero Compiled Not mapped

No declaration docstring.

def zero : ProgressiveL2Integrand filtration mu T where
  process := fun _ _ => 0
  progressive := isStronglyProgressive_const filtration 0
  memLp := MemLp.zero

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Algebra.lean:25published source at 7bcd37294df1

def AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Algebra.add Compiled Not mapped

No declaration docstring.

def add (eta xi : ProgressiveL2Integrand filtration mu T) :
    ProgressiveL2Integrand filtration mu T where
  process := fun t omega => eta.process t omega + xi.process t omega
  progressive := eta.progressive.add xi.progressive
  memLp := eta.memLp.add xi.memLp

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Algebra.lean:30published source at 7bcd37294df1

def AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Algebra.neg Compiled Not mapped

No declaration docstring.

def neg (eta : ProgressiveL2Integrand filtration mu T) :
    ProgressiveL2Integrand filtration mu T where
  process := fun t omega => -eta.process t omega
  progressive := eta.progressive.neg
  memLp := eta.memLp.neg

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Algebra.lean:36published source at 7bcd37294df1

def AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Algebra.sub Compiled Not mapped

No declaration docstring.

def sub (eta xi : ProgressiveL2Integrand filtration mu T) :
    ProgressiveL2Integrand filtration mu T where
  process := fun t omega => eta.process t omega - xi.process t omega
  progressive := eta.progressive.sub xi.progressive
  memLp := eta.memLp.sub xi.memLp

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Algebra.lean:42published source at 7bcd37294df1

def AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Algebra.smul Compiled Not mapped

No declaration docstring.

def smul (c : ℝ) (eta : ProgressiveL2Integrand filtration mu T) :
    ProgressiveL2Integrand filtration mu T where
  process := fun t omega => c * eta.process t omega
  progressive := fun i => (eta.progressive i).const_smul c
  memLp := eta.memLp.const_smul c

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Algebra.lean:48published source at 7bcd37294df1

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Algebra.zero_process Compiled Not mapped

No declaration docstring.

@[simp] theorem zero_process :
    (zero : ProgressiveL2Integrand filtration mu T).process = 0 :=
  rfl

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Algebra.lean:54published source at 7bcd37294df1

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Algebra.add_process Compiled Not mapped

No declaration docstring.

@[simp] theorem add_process (eta xi : ProgressiveL2Integrand filtration mu T) :
    (add eta xi).process = eta.process + xi.process :=
  rfl

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Algebra.lean:58published source at 7bcd37294df1

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Algebra.neg_process Compiled Not mapped

No declaration docstring.

@[simp] theorem neg_process (eta : ProgressiveL2Integrand filtration mu T) :
    (neg eta).process = -eta.process :=
  rfl

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Algebra.lean:62published source at 7bcd37294df1

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Algebra.sub_process Compiled Not mapped

No declaration docstring.

@[simp] theorem sub_process (eta xi : ProgressiveL2Integrand filtration mu T) :
    (sub eta xi).process = eta.process - xi.process :=
  rfl

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Algebra.lean:66published source at 7bcd37294df1

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Algebra.smul_process Compiled Not mapped

No declaration docstring.

@[simp] theorem smul_process (c : ℝ)
    (eta : ProgressiveL2Integrand filtration mu T) :
    (smul c eta).process = c • eta.process :=
  rfl

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Algebra.lean:70published source at 7bcd37294df1

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Algebra.toLp_zero Compiled Not mapped

No declaration docstring.

@[simp] theorem toLp_zero :
    (zero : ProgressiveL2Integrand filtration mu T).toLp = 0 :=
  rfl

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Algebra.lean:75published source at 7bcd37294df1

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Algebra.toLp_add Compiled Not mapped

No declaration docstring.

theorem toLp_add (eta xi : ProgressiveL2Integrand filtration mu T) :
    (add eta xi).toLp = eta.toLp + xi.toLp :=
  rfl

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Algebra.lean:79published source at 7bcd37294df1

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Algebra.toLp_neg Compiled Not mapped

No declaration docstring.

theorem toLp_neg (eta : ProgressiveL2Integrand filtration mu T) :
    (neg eta).toLp = -eta.toLp :=
  rfl

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Algebra.lean:83published source at 7bcd37294df1

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Algebra.toLp_sub Compiled Not mapped

No declaration docstring.

theorem toLp_sub (eta xi : ProgressiveL2Integrand filtration mu T) :
    (sub eta xi).toLp = eta.toLp - xi.toLp :=
  rfl

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Algebra.lean:87published source at 7bcd37294df1

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Algebra.toLp_smul Compiled Not mapped

No declaration docstring.

theorem toLp_smul (c : ℝ) (eta : ProgressiveL2Integrand filtration mu T) :
    (smul c eta).toLp = c • eta.toLp :=
  rfl

/-- Restriction commutes with subtraction in product-space `L2`. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Algebra.lean:91published source at 7bcd37294df1Open detailed card

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Algebra.toLp_restrictAt_sub Compiled Not mapped

- Restriction commutes with subtraction in product-space `L2`.

theorem toLp_restrictAt_sub (eta xi : ProgressiveL2Integrand filtration mu T)
    (t : ℝ≥0) :
    ((sub eta xi).restrictAt t).toLp =
      (eta.restrictAt t).toLp - (xi.restrictAt t).toLp := by
  simp only [ProgressiveL2Integrand.toLp]
  rw [← MemLp.toLp_sub]
  apply MemLp.toLp_congr
  filter_upwards [] with z
  by_cases hzt : z.2 < t
  · simp [processFunction, ProgressiveL2Integrand.restrictProcess, hzt, sub]
  · simp [processFunction, ProgressiveL2Integrand.restrictProcess, hzt, sub]

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Algebra.lean:96published source at 7bcd37294df1

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Algebra.toLp_restrictAt_add Compiled Not mapped

No declaration docstring.

theorem toLp_restrictAt_add (eta xi : ProgressiveL2Integrand filtration mu T)
    (t : ℝ≥0) :
    ((add eta xi).restrictAt t).toLp =
      (eta.restrictAt t).toLp + (xi.restrictAt t).toLp := by
  simp only [ProgressiveL2Integrand.toLp]
  rw [← MemLp.toLp_add]
  apply MemLp.toLp_congr
  filter_upwards [] with z
  by_cases hzt : z.2 < t
  · simp [processFunction, ProgressiveL2Integrand.restrictProcess, hzt, add]
  · simp [processFunction, ProgressiveL2Integrand.restrictProcess, hzt, add]

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Algebra.lean:108published source at 7bcd37294df1

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Algebra.toLp_restrictAt_smul Compiled Not mapped

No declaration docstring.

theorem toLp_restrictAt_smul (c : ℝ)
    (eta : ProgressiveL2Integrand filtration mu T) (t : ℝ≥0) :
    ((smul c eta).restrictAt t).toLp = c • (eta.restrictAt t).toLp := by
  simp only [ProgressiveL2Integrand.toLp]
  rw [← MemLp.toLp_const_smul]
  apply MemLp.toLp_congr
  filter_upwards [] with z
  by_cases hzt : z.2 < t
  · simp [processFunction, ProgressiveL2Integrand.restrictProcess, hzt, smul]
  · simp [processFunction, ProgressiveL2Integrand.restrictProcess, hzt, smul]

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Algebra.lean:120published source at 7bcd37294df1

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Algebra.toLp_restrictAt_zero Compiled Not mapped

No declaration docstring.

@[simp] theorem toLp_restrictAt_zero (t : ℝ≥0) :
    ((zero : ProgressiveL2Integrand filtration mu T).restrictAt t).toLp = 0 := by
  apply norm_eq_zero.mp
  have h :=
    (zero : ProgressiveL2Integrand filtration mu T).norm_restrictAt_le t
  exact le_antisymm (by simpa only [toLp_zero, norm_zero] using h) (norm_nonneg _)

/-- Restricting both integrands cannot increase their product-space `L2`
distance. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Algebra.lean:131published source at 7bcd37294df1

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Algebra.norm_restrictAt_sub_le Compiled Not mapped

- Restricting both integrands cannot increase their product-space `L2` distance.

theorem norm_restrictAt_sub_le
    (eta xi : ProgressiveL2Integrand filtration mu T) (t : ℝ≥0) :
    ‖(eta.restrictAt t).toLp - (xi.restrictAt t).toLp‖ ≤
      ‖eta.toLp - xi.toLp‖ := by
  rw [← toLp_restrictAt_sub, ← toLp_sub]
  exact (sub eta xi).norm_restrictAt_le t

/-- Equality in product-space `L2` is preserved by every deterministic time
restriction.  This is the congruence principle used to turn completed
integrand identities into process-level Itô identities. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Algebra.lean:140published source at 7bcd37294df1

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Algebra.restrictAt_toLp_eq_of_toLp_eq Compiled Not mapped

- Equality in product-space `L2` is preserved by every deterministic time restriction. This is the congruence principle used to turn completed integrand identities into process-level Itô identities.

theorem restrictAt_toLp_eq_of_toLp_eq
    (eta xi : ProgressiveL2Integrand filtration mu T)
    (hEq : eta.toLp = xi.toLp) (t : ℝ≥0) :
    (eta.restrictAt t).toLp = (xi.restrictAt t).toLp := by
  have hle := norm_restrictAt_sub_le eta xi t
  have hzero : ‖eta.toLp - xi.toLp‖ = 0 := by
    rw [hEq]
    simp
  have hnorm : ‖(eta.restrictAt t).toLp - (xi.restrictAt t).toLp‖ = 0 := by
    apply le_antisymm
    · simpa only [hzero] using hle
    · exact norm_nonneg _
  exact sub_eq_zero.mp (norm_eq_zero.mp hnorm)

end ProgressiveL2Algebra
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Algebra.lean:150published source at 7bcd37294df1