Documentation

BGW.StableTrees.DiscreteHeightApproxOccupationContinuity

Dominated convergence for finite-path occupations #

Lebesgue integration stays in the original time coordinate. Pointwise J1 continuity of gaps away from jump times and null boundary levels suffices.

source
noncomputable def BGW.StableTrees.DiscreteHeightApprox.finiteGap (T t : NNReal) (f : Skorokhod.D ↑T ℝ) (s : ℝ) :
ℝ

The future-infimum gap of a constantly extended finite path.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem BGW.StableTrees.DiscreteHeightApprox.measurable_finiteGap_time (T t : NNReal) (f : Skorokhod.D ↑T ℝ) :
    Measurable (finiteGap T t f)

    The finite-path gap is measurable in its real time coordinate.

    source
    theorem BGW.StableTrees.DiscreteHeightApprox.continuousAt_finiteHeightApprox_of_ae (T t : NNReal) (ε : ℝ) {f : Skorokhod.D ↑T ℝ} (hc : ∀ᵐ (s : ℝ), s ∈ Set.Icc 0 ↑t → ContinuousAt (fun (g : Skorokhod.D ↑T ℝ) => finiteGap T t g s) f) (hb : MeasureTheory.volume {s : ℝ | s ∈ Set.Icc 0 ↑t ∧ finiteGap T t f s = ε} = 0) :
    ContinuousAt (finiteHeightApprox T t ε) f

    Dominated convergence gives occupation continuity whenever the gap is pointwise continuous almost everywhere in the window and the boundary level has zero measure.

    source
    theorem BGW.StableTrees.DiscreteHeightApprox.continuousAt_of_leftLim_eq {T : ℝ} (f : Skorokhod.D T ℝ) (s : ↑(Set.Icc 0 T)) (hs : Function.leftLim (⇑f) s = f s) :
    ContinuousAt (⇑f) s

    A càdlàg path is continuous where its left limit agrees with its value.

    source
    theorem BGW.StableTrees.DiscreteHeightApprox.ae_continuousAt_finiteGap (T t : NNReal) (ht : t ≤ T) {f : Skorokhod.D ↑T ℝ} (htf : t = T ∨ ContinuousAt ⇑f ⟨↑t, ⋯⟩) :
    ∀ᵐ (s : ℝ), s ∈ Set.Icc 0 ↑t → ContinuousAt (fun (g : Skorokhod.D ↑T ℝ) => finiteGap T t g s) f

    At almost every real time in the window, the finite-path gap is J1-continuous.

    source
    theorem BGW.StableTrees.DiscreteHeightApprox.continuousAt_finiteHeightApprox (T t : NNReal) (ht : t ≤ T) (ε : ℝ) {f : Skorokhod.D ↑T ℝ} (htf : t = T ∨ ContinuousAt ⇑f ⟨↑t, ⋯⟩) (hb : MeasureTheory.volume {s : ℝ | s ∈ Set.Icc 0 ↑t ∧ finiteGap T t f s = ε} = 0) :
    ContinuousAt (finiteHeightApprox T t ε) f

    The finite occupation functional is J1-continuous away from null boundary levels.