Documentation

BGW.StableTrees.ExcursionHeightPassagePastSlope

Predictable left passage slopes at fixed levels #

The extended left passage time and its deterministic delays are predictable. Hence failure of convergence of their dyadic left difference quotients is a predictable event. Infinite passage times are retained throughout this construction.

The extended left passage process is monotone and lies between each strictly earlier passage and the current passage. A doubled-cutoff comparison transfers the full-filter zero-slope estimate to its finite reading, without assuming equality at fixed levels.

source
theorem BGW.StableTrees.measurable_predictable_passagePast :
Measurable fun (p : NNReal × Skorokhod.DLoc) => passagePast p.1 p.2

The extended left passage time is predictable.

source
theorem BGW.StableTrees.measurable_predictable_passagePast_delay (δ : NNReal) :
Measurable fun (p : NNReal × Skorokhod.DLoc) => passagePast (p.1 - δ) p.2

A deterministic delay of the extended left passage time is predictable.

source
noncomputable def BGW.StableTrees.excursionHeightLeftSlopeBad :
Set (NNReal × Skorokhod.DLoc)

Failure of vanishing dyadic left slopes of the extended passage process.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem BGW.StableTrees.measurableSet_excursionHeightLeftSlopeBad :
    MeasurableSet excursionHeightLeftSlopeBad

    The bad left-slope event is predictable, so general predictable compensation applies.

    source
    theorem BGW.StableTrees.monotone_passagePast (f : Skorokhod.DLoc) :
    Monotone fun (x : NNReal) => passagePast x f

    The extended left passage process is monotone on every path.

    source
    theorem BGW.StableTrees.ae_passageTimeMinus_order_bounds {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) :
    ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), (Monotone fun (x : NNReal) => passageTimeMinus x f) ∧ (∀ (x : NNReal), passageTimeMinus x f ≤ passageTime x f) ∧ ∀ (a b : NNReal), a < b → passageTime a f ≤ passageTimeMinus b f

    Finite left passage values have monotonicity and the usual earlier/current bounds.

    source
    theorem BGW.StableTrees.ae_tendsto_passageTimeMinus_leftSlope {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (x : NNReal) (hx : 0 < x) :
    ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), Filter.Tendsto (fun (ε : ℝ) => (↑(passageTimeMinus x f) - ↑(passageTimeMinus (x - ε.toNNReal) f)) / ε) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

    At a fixed positive level the finite left passage process has a zero full left slope.