Finite-range stopping-time integrand terms
DefinitionKLSModular_LevyStochCalc_Brownian_ItoOptionalStoppingVendored from the LevyStochCalc library at https://github.com/cgarryZA/LevyStochCalc, commit 984dbf0b790031eac05d56fe5a84b65e15e1e932. Under a probability measure , hitInd τ c is the indicator of the event , cutTerm τ H c t is this indicator multiplied by the interval indicator and , and indTerm τ H c t is the same interval restriction with unit weight. The auxiliary theorem energy_lt_top_of_abs_le transfers finite energy from to under the pointwise domination .
Original module imports
import LevyStochCalc.Brownian.ItoFinsetSum
import LevyStochCalc.Brownian.ItoPullOut
import LevyStochCalc.Probability.StoppedProgressive
Original declaration excerpt
Shown in the original module context.
noncomputable def hitInd (c : ℝ) : Ω → ℝ :=
Set.indicator {ω | τ ω = ((c : ℝ) : WithTop ℝ)} fun _ => (1 : ℝ)
Module navigation
Direct project imports: LevyStochCalc/Brownian/ItoFinsetSum, LevyStochCalc/Brownian/ItoPullOut, LevyStochCalc/Probability/StoppedProgressive.
Theorems in source order:
Project result: The KLS conjecture.
Original module · LevyStochCalc.Brownian.ItoOptionalStopping · Frozen source 408915f.
import Definitions.Def_KLSModular_LevyStochCalc_Brownian_ItoFinsetSum
import Definitions.Def_KLSModular_LevyStochCalc_Brownian_ItoPullOut
import Definitions.Def_KLSModular_LevyStochCalc_Probability_StoppedProgressive
/-
Copyright (c) 2026 Christian Garry. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Christian Garry
-/
-- Vendored from https://github.com/cgarryZA/LevyStochCalc at commit 984dbf0b790031eac05d56fe5a84b65e15e1e932 (upstream path LevyStochCalc/Brownian/ItoOptionalStopping.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
namespace LevyStochCalc
namespace Brownian
namespace Ito
open MeasureTheory ProbabilityTheory
open scoped NNReal ENNReal
universe u
variable {Ω : Type u} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
omit [IsProbabilityMeasure P] in
/-- Square-integrability transfers along a pointwise domination of the integrands. -/
theorem energy_lt_top_of_abs_le {K G : Ω → ℝ → ℝ} (h : ∀ ω s, |K ω s| ≤ |G ω s|)
(hq : ∀ T, 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
(‖G ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤) :
∀ T, 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
(‖K ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤ := by
intro T hT
refine lt_of_le_of_lt (lintegral_mono fun ω => lintegral_mono fun s => ?_) (hq T hT)
have hle : (‖K ω s‖₊ : ℝ≥0∞) ≤ (‖G ω s‖₊ : ℝ≥0∞) := by
refine ENNReal.coe_le_coe.mpr ?_
rw [← NNReal.coe_le_coe]
simpa [Real.norm_eq_abs] using h ω s
gcongr
section Stopped
variable (τ : Ω → WithTop ℝ)
/-- The indicator of the event that the stopping time takes the value `c`. -/
noncomputable def hitInd (c : ℝ) : Ω → ℝ :=
Set.indicator {ω | τ ω = ((c : ℝ) : WithTop ℝ)} fun _ => (1 : ℝ)
/-- The part of the integrand that the cut at `τ = c` removes from the window `(c, t]`. -/
noncomputable def cutTerm (H : Ω → ℝ → ℝ) (c t : ℝ) : Ω → ℝ → ℝ :=
fun ω s => hitInd τ c ω * indIoc Ω c t ω s * H ω s
/-- The integrand restricted to a window, as a `cutTerm` with unit weight. -/
noncomputable def indTerm (H : Ω → ℝ → ℝ) (c t : ℝ) : Ω → ℝ → ℝ :=
fun ω s => indIoc Ω c t ω s * H ω s
end Stopped
end Ito
end Brownian
end LevyStochCalc