Fixed-time height approximation

Reversal identifies occupation approximations outside the countable set of jumps. Prefix events transport along the equality of restricted-path laws, yielding both almost sure convergence along the public sequence and convergence in measure.

theorem BGW.StableTrees.heightApprox_eq_supOccupation_reversed (f : Skorokhod.DLoc) (hf : ∀ (r : NNReal), Function.leftLim (↑f) r ≤ ↑f r) (t : NNReal) (ε : ℝ) : heightApprox ε f t = supOccupation ε (reversedAt t f) t

Occupation reversal holds pathwise for paths with nonnegative jumps.

theorem BGW.StableTrees.ae_heightApprox_eq_supOccupation_reversed {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t : NNReal) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (ε : ℝ), 0 < ε → heightApprox ε f t = supOccupation ε (reversedAt t f) t

Identification (a.s. for each fixed t, all ε > 0 at once): the interval-infimum approximation is the H01 occupation approximation of the reversed process.

theorem BGW.StableTrees.rawFiltration_le_restrict_comap (t : NNReal) : ↑Skorokhod.DLoc.rawFiltration t ≤ MeasurableSpace.comap (Skorokhod.DLoc.restrict t) inferInstance

The raw filtration is contained in the sigma-algebra of the restricted path.

theorem BGW.StableTrees.measurable_supOccupation_prefix (ε : ℝ) (t : NNReal) : Measurable fun (f : Skorokhod.DLoc) => supOccupation ε f t

The occupation at a fixed horizon is measurable from the restricted path.

theorem BGW.StableTrees.measurable_supLocalTime_prefix (θ : ℝ) (t : NNReal) : Measurable fun (f : Skorokhod.DLoc) => supLocalTime θ f t

The supremum local time at a fixed horizon is measurable from the restricted path.

theorem BGW.StableTrees.ae_reversedAt_of_prefix {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {t : NNReal} (ht : 0 < t) {p : Skorokhod.DLoc → Prop} (hp : MeasurableSet {f : Skorokhod.DLoc | p f}) (ha : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), p f) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), p (reversedAt t f)

A measurable almost sure prefix property transports to the reversed prefix.

theorem BGW.StableTrees.heightApprox_zero (ε : ℝ) (f : Skorokhod.DLoc) : heightApprox ε f 0 = 0

The height approximation vanishes at its initial time for every path and cutoff.

theorem BGW.StableTrees.height_zero (θ : ℝ) (f : Skorokhod.DLoc) : height θ f 0 = 0

The height starts at zero on every path, including exceptional paths.

theorem BGW.StableTrees.ae_tendsto_heightApprox_supEps {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t : NNReal) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), Filter.Tendsto (fun (k : ℕ) => heightApprox (supEps θ k) f t) Filter.atTop (nhds (height θ f t))

A.s. convergence along the deterministic sequence supEps θ, for each fixed t (the null set depends on t).

theorem BGW.StableTrees.heightApprox_tendstoInMeasure {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t : NNReal) : MeasureTheory.TendstoInMeasure (↑(stableLocalLaw θ)) (fun (ε : ℝ) (f : Skorokhod.DLoc) => heightApprox ε f t) (nhdsWithin 0 (Set.Ioi 0)) fun (f : Skorokhod.DLoc) => height θ f t

Convergence in probability for each fixed t along the full filter ε ↓ 0.

theorem BGW.StableTrees.ae_heightRaw_eq {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t : NNReal) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), 0 ≤ height θ f t ∧ heightRaw θ f t = ENNReal.ofReal (height θ f t)

The raw height is a.s. the finite nonnegative height, for each fixed t.