Stopped-process simplification rules
DefinitionKLSModular_BrownianMotion_Auxiliary_StoppedProcessfunctional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-contextvendored-brownianmotion
Vendored from the BrownianMotion library (https://github.com/RemyDegenne/brownian-motion, commit a7ad7af662044313bc80a7c0756360fb3745f931). stoppedProcess_of_eq_coe identifies a stopped process at a stopping time equal to an ordinary index with the original process evaluated at min s t. The bundle also proves that stoppedValue distributes over addition, negation, and subtraction.
Original module imports
public import BrownianMotion.Auxiliary.Indistinguishable
public import BrownianMotion.StochasticIntegral.Cadlag
public import Mathlib.Probability.Process.Stopping
Original declaration excerpt
Shown in the original module context.
@[simp]
lemma stoppedProcess_of_eq_coe (s : ι) (hτ : τ ω = t) :
stoppedProcess X τ s ω = X (min s t) ω := by
obtain h | h := le_total s t <;> simp [stoppedProcess, hτ, h]
Module navigation
Direct project imports: BrownianMotion/Auxiliary/Indistinguishable, BrownianMotion/StochasticIntegral/Cadlag.
Project result: The KLS conjecture.
Original module · BrownianMotion.Auxiliary.StoppedProcess · Frozen source 408915f.
Definition code
import Definitions.Def_KLSModular_BrownianMotion_Auxiliary_Indistinguishable
import Definitions.Def_KLSModular_BrownianMotion_StochasticIntegral_Cadlag
import Mathlib.Probability.Process.Stopping
-- Vendored from https://github.com/RemyDegenne/brownian-motion at commit a7ad7af662044313bc80a7c0756360fb3745f931 (upstream path BrownianMotion/Auxiliary/StoppedProcess.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
section
open MeasureTheory Filter
open scoped ENNReal Topology
namespace MeasureTheory
variable {ι Ω E : Type*} {mΩ : MeasurableSpace Ω} {P : Measure Ω} [Nonempty ι]
{τ : Ω → WithTop ι} {ω : Ω} {t : ι} {X Y : ι → Ω → E}
section stoppedProcess
variable [LinearOrder ι]
@[simp]
lemma stoppedProcess_of_eq_coe (s : ι) (hτ : τ ω = t) :
stoppedProcess X τ s ω = X (min s t) ω := by
obtain h | h := le_total s t <;> simp [stoppedProcess, hτ, h]
end stoppedProcess
namespace stoppedValue
@[simp] lemma add [Add E] {u v : ι → Ω → E} {τ : Ω → WithTop ι} :
stoppedValue (u + v) τ = stoppedValue u τ + stoppedValue v τ := rfl
@[simp] lemma neg [Neg E] {u : ι → Ω → E} {τ : Ω → WithTop ι} :
stoppedValue (-u) τ = -stoppedValue u τ := rfl
@[simp] lemma sub [Sub E] {u v : ι → Ω → E} {τ : Ω → WithTop ι} :
stoppedValue (u - v) τ = stoppedValue u τ - stoppedValue v τ := rfl
end stoppedValue
end MeasureTheory
Source
Lean source: https://github.com/RemyDegenne/brownian-motion/blob/a7ad7af662044313bc80a7c0756360fb3745f931/BrownianMotion/Auxiliary/StoppedProcess.lean#L26-L133 (repository human-ai-mathematics/kls-lean, commit 408915f, module `BrownianMotion.Auxiliary.StoppedProcess`, definition bundle `KLSModular_BrownianMotion_Auxiliary_StoppedProcess`; the repository is private at upload time). Vendored from https://github.com/RemyDegenne/brownian-motion at commit a7ad7af662044313bc80a7c0756360fb3745f931 (Apache-2.0; upstream copyright notice retained in the Lean text).