Documentation

BGW.StableTrees.BridgePrefix

Stable bridge prefix laws #

The stable transition density defines normalized, consistent changes of measure on every strict prefix of the unit interval.

References: J. Bertoin, Lévy Processes (1996), ch. VIII (bridges); L. Chaumont, Excursion normalisée, méandre et pont pour les processus de Lévy stables, Bull. Sci. Math. 121 (1997); item C31 of CLASSICAL_THEORY_INPUTS.md.

source
noncomputable def BGW.StableTrees.bridgePrefixWeight (θ a : ℝ) (ha : 0 ≤ a) (f : Skorokhod.D a ℝ) :
ℝ

The prefix weight wₐ(f) = p_{1-a}(-f(a)) / p₁(0).

Equations
Instances For
    source
    noncomputable def BGW.StableTrees.bridgePrefixLaw (θ a : ℝ) (ha : 0 ≤ a) (P : MeasureTheory.Measure (Skorokhod.D a ℝ)) :
    MeasureTheory.Measure (Skorokhod.D a ℝ)

    The prefix measure obtained by weighting a path law by bridgePrefixWeight.

    Equations
    Instances For
      source
      theorem BGW.StableTrees.bridgePrefixWeight_nonneg {θ a : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (ha : 0 ≤ a) (ha1 : a < 1) (f : Skorokhod.D a ℝ) :
      0 ≤ bridgePrefixWeight θ a ha f

      The bridge prefix weight is nonnegative whenever a < 1.

      source
      theorem BGW.StableTrees.measurable_bridgePrefixWeight {θ a : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (ha : 0 ≤ a) :
      Measurable (bridgePrefixWeight θ a ha)

      The bridge prefix weight is measurable for the Borel σ-algebra on path space.

      source
      theorem BGW.StableTrees.bridgePrefixWeight_le {θ a : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (ha : 0 ≤ a) (ha1 : a < 1) :
      ∃ (C : ℝ), ∀ (f : Skorokhod.D a ℝ), bridgePrefixWeight θ a ha f ≤ C

      For each fixed a < 1, the bridge prefix weight is bounded.

      source
      theorem BGW.StableTrees.bridgePrefix_mass_one {θ a : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (ha : 0 < a) (ha1 : a < 1) {P : MeasureTheory.ProbabilityMeasure (Skorokhod.D a ℝ)} (hP : IsStableLevyLaw θ a P) :
      ∫⁻ (f : Skorokhod.D a ℝ), ENNReal.ofReal (bridgePrefixWeight θ a ⋯ f) ∂↑P = 1

      Mass one. Every stable Lévy law on [0,a] integrates the bridge weight to one.

      source
      theorem BGW.StableTrees.isProbabilityMeasure_bridgePrefixLaw {θ a : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (ha : 0 < a) (ha1 : a < 1) {P : MeasureTheory.ProbabilityMeasure (Skorokhod.D a ℝ)} (hP : IsStableLevyLaw θ a P) :
      MeasureTheory.IsProbabilityMeasure (bridgePrefixLaw θ a ⋯ ↑P)

      A normalized bridge prefix is a probability measure.

      source
      theorem BGW.StableTrees.bridgePrefixLaw_unique {θ a : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (ha : 0 < a) {P Q : MeasureTheory.ProbabilityMeasure (Skorokhod.D a ℝ)} (hP : IsStableLevyLaw θ a P) (hQ : IsStableLevyLaw θ a Q) :
      bridgePrefixLaw θ a ⋯ ↑P = bridgePrefixLaw θ a ⋯ ↑Q

      The prefix law does not depend on the choice of the stable law P (uniqueness).

      source
      theorem BGW.StableTrees.bridgePrefix_consistent {θ a b : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (ha : 0 < a) (hab : a ≤ b) (hb : b < 1) {Pa : MeasureTheory.ProbabilityMeasure (Skorokhod.D a ℝ)} {Pb : MeasureTheory.ProbabilityMeasure (Skorokhod.D b ℝ)} (hPa : IsStableLevyLaw θ a Pa) (hPb : IsStableLevyLaw θ b Pb) :
      MeasureTheory.Measure.map (Skorokhod.restrict hab) (bridgePrefixLaw θ b ⋯ ↑Pb) = bridgePrefixLaw θ a ⋯ ↑Pa

      Consistency at the level of measures on D a ℝ. Restricting the tilted law at b gives the tilted law at a.

      source
      theorem BGW.StableTrees.bridgePrefix_family {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (P : (a : ℝ) → MeasureTheory.ProbabilityMeasure (Skorokhod.D a ℝ)) (hP : ∀ (a : ℝ), 0 < a → IsStableLevyLaw θ a (P a)) (a b : ℝ) (ha : 0 < a) (hab : a ≤ b) (_hb : b < 1) :
      MeasureTheory.IsProbabilityMeasure (bridgePrefixLaw θ a ⋯ ↑(P a)) ∧ MeasureTheory.Measure.map (Skorokhod.restrict hab) (bridgePrefixLaw θ b ⋯ ↑(P b)) = bridgePrefixLaw θ a ⋯ ↑(P a)

      Abstract-family form: the bridge prefix laws are probability measures and consistent.