OAI/Probability/FKMaps/TraceLimit.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FKCRT.SimpleWalk.segments line 12

    Source documentation

    Durations followed by a terminal first-hitting segment.

    def segments {m : ℕ} (d b : Fin m → ℕ) : List (ℕ×ℕ) :=
…
  2. lemma OAI.FKCRT.SimpleWalk.segments_cons line 15
  3. lemma OAI.FKCRT.SimpleWalk.traceSize_segments line 19
  4. def OAI.FKCRT.SimpleWalk.normalizedTrace line 24
  5. lemma OAI.FKCRT.SimpleWalk.normalizedTrace_cons line 28
  6. def OAI.FKCRT.SimpleWalk.remaining line 43

    Source documentation

    Macroscopic bridge parameters expressed directly in successive durations.

    def remaining {m : ℕ} (s : Fin m → ℝ) (r : ℝ) (i : Fin m) : ℝ :=
…
  7. def OAI.FKCRT.SimpleWalk.durationRatio line 46
  8. def OAI.FKCRT.SimpleWalk.durationVariance line 49
  9. lemma OAI.FKCRT.SimpleWalk.remaining_zero line 52
  10. lemma OAI.FKCRT.SimpleWalk.remaining_succ line 59
  11. lemma OAI.FKCRT.SimpleWalk.remaining_pos line 65
  12. lemma OAI.FKCRT.SimpleWalk.sum_ratio_tendsto line 70
  13. lemma OAI.FKCRT.SimpleWalk.even_int_cast line 76
  14. lemma OAI.FKCRT.SimpleWalk.even_int_terminal line 78
  15. lemma OAI.FKCRT.SimpleWalk.firstHit_eventually_ne_zero line 86
  16. lemma OAI.FKCRT.SimpleWalk.pathMass_nonneg line 100
  17. lemma OAI.FKCRT.SimpleWalk.chainDensity_ne_top line 104
  18. lemma OAI.FKCRT.SimpleWalk.scaledTrace_limit_positive line 114

    Source documentation

    Interior-start conditioned trace densities from the exact killed kernels.

    lemma scaledTrace_limit_positive (m : ℕ) {d b : ℕ → Fin m → ℕ} {R T a : ℕ → ℕ}
    {s x : Fin m → ℝ} {r z : ℝ}
    (hr : 0<r) (hz : 0<z) (hs : ∀ i,0<s i) (hx : ∀ i,0<x i)
    (hR : Tendsto R atTop atTop) (hT : Tendsto T atTop atTop)
    (hd : ∀ i,Tendsto (fun n => d n i) atTop atTop)
    (hrR : Tendsto (fun n => ((R n:ℝ)+1)/(T n:ℝ)) atTop (𝓝 r))
    (hrd : ∀ i,Tendsto (fun n => (d n i:ℝ)/(T n:ℝ)) atTop (𝓝 (s i)))
    (hRe : ∀ n,Even (R n)) (hde : ∀ n i,Even (d n i))
    (hae : ∀ n,Even (a n)) (hbe : ∀ n i,Even (b n i))
    (ha : Tendsto (fun n => (a n:ℝ)/Real.sqrt (T n:ℝ)) atTop (𝓝 z))
    (hb : ∀ i,Tendsto (fun n => (b n i:ℝ)/Real.sqrt (T n:ℝ)) atTop (𝓝 (x i))) :
    Tendsto (fun n => ENNReal.ofReal ((Real.sqrt (T n:ℝ)/2)^m*
…
  19. lemma OAI.FKCRT.SimpleWalk.scaledTrace_limit_zero line 188

    Source documentation

    Entrance-start trace densities, including the singular zero-radius initial law.

    lemma scaledTrace_limit_zero (m : ℕ) {d b : ℕ → Fin m → ℕ} {R T : ℕ → ℕ}
    {s x : Fin m → ℝ} {r : ℝ}
    (hr : 0<r) (hs : ∀ i,0<s i) (hx : ∀ i,0<x i)
    (hR : Tendsto R atTop atTop) (hT : Tendsto T atTop atTop)
    (hd : ∀ i,Tendsto (fun n => d n i) atTop atTop)
    (hrR : Tendsto (fun n => ((R n:ℝ)+1)/(T n:ℝ)) atTop (𝓝 r))
    (hrd : ∀ i,Tendsto (fun n => (d n i:ℝ)/(T n:ℝ)) atTop (𝓝 (s i)))
    (hRe : ∀ n,Even (R n)) (hde : ∀ n i,Even (d n i))
    (hbe : ∀ n i,Even (b n i))
    (hb : ∀ i,Tendsto (fun n => (b n i:ℝ)/Real.sqrt (T n:ℝ)) atTop (𝓝 (x i))) :
    Tendsto (fun n => ENNReal.ofReal ((Real.sqrt (T n:ℝ)/2)^m*
      normalizedTrace 0 (R n) (d n) (b n))) atTop
…

    Mentions: OAI.FKCRT.SimpleWalk.normalizedTrace

  20. lemma OAI.FKCRT.SimpleWalk.sum_differences_nat line 276
  21. lemma OAI.FKCRT.SimpleWalk.located_differences line 293
  22. lemma OAI.FKCRT.SimpleWalk.sum_gridDurations line 313
  23. lemma OAI.FKCRT.SimpleWalk.grid_total line 320
  24. lemma OAI.FKCRT.SimpleWalk.grid_observed line 327
  25. lemma OAI.FKCRT.SimpleWalk.gridRemainder_ratio line 338
  26. lemma OAI.FKCRT.SimpleWalk.nat_atTop_of_ratio line 352
  27. def OAI.FKCRT.Radial.bridgeRatio line 374
  28. def OAI.FKCRT.Radial.bridgeVariance line 375
  29. def OAI.FKCRT.Radial.bridgeResidual line 376
  30. lemma OAI.FKCRT.Radial.bridgeRatio_pos line 379
  31. lemma OAI.FKCRT.Radial.bridgeVariance_pos line 384
  32. lemma OAI.FKCRT.Radial.bridgeResidual_gaussian line 389
  33. lemma OAI.FKCRT.Radial.integral_bridgeResidual line 402
  34. lemma OAI.FKCRT.Radial.covariance_bridgeResidual_earlier line 411
  35. lemma OAI.FKCRT.Radial.variance_bridgeResidual line 428
  36. lemma OAI.FKCRT.Radial.bridgeResidual_hasLaw line 451
  37. def OAI.FKCRT.Radial.innovation line 461

    Source documentation

    The standardized regression innovations at arbitrary increasing interior times.

    def innovation {Ω : Type*} (B : ℝ≥0 → Ω → ℝ) {m : ℕ}
    (u : Fin (m+1) → unitInterval) (i : Fin m) (ω : Ω) : ℝ :=
…
  38. lemma OAI.FKCRT.Radial.innovation_hasLaw line 466
  39. lemma OAI.FKCRT.Radial.innovations_independent line 485
  40. lemma OAI.FKCRT.Radial.innovations_gaussian line 532
  41. lemma OAI.FKCRT.Radial.independent_innovations line 539
  42. theorem OAI.FKCRT.Radial.vector_innovations_law line 554

    Source documentation

    Regression innovations are independent not only in time but across the three source Brownian coordinates; no radial-process theorem is taken as an assumption.

    theorem vector_innovations_law {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω}
    {B : Fin 3 → ℝ≥0 → Ω → ℝ} (hB : ∀ k,IsPreBrownianReal (B k) P)
    (hI : iIndepFun (fun i ω t => B i t ω) P) {m : ℕ}
    (u : Fin (m+1) → unitInterval) (hu : StrictMono u) (h1 : ∀ i,(u i:ℝ)<1) :
    HasLaw (fun ω i => (toLp 2 (fun k => innovation (B k) u i ω) : Space))
      (Measure.pi (fun _ : Fin m => stdGaussian Space)) P := by
…

    Mentions: OAI.FKCRT.Radial.innovation, OAI.FKCRT.Radial.Space

  43. lemma OAI.FKCRT.Radial.chain_reconstruct line 589

    Source documentation

    Reconstruction of a chronological chain from its standardized innovations.

    lemma chain_reconstruct (m : ℕ) (x : Fin (m+1) → Space) (a t : Fin m → ℝ)
    (ht : ∀ i,0<t i) :
    chain (x 0) a t (fun i => (Real.sqrt (t i))⁻¹ • (x i.succ-a i • x i.castSucc)) =
      Fin.tail x := by
…

    Mentions: OAI.FKCRT.Radial.Space, OAI.FKCRT.Radial.chain

  44. def OAI.FKCRT.Radial.bridgeVector line 621
  45. def OAI.FKCRT.Radial.bridgeDensity line 624
  46. lemma OAI.FKCRT.Radial.vector_residual line 628
  47. lemma OAI.FKCRT.Radial.norm_bridgeVector line 637
  48. theorem OAI.FKCRT.Radial.lintegral_standardExcursion line 649

    Source documentation

    Exact finite-dimensional density of the source standard excursion (the norm of three independent bridges), at every increasing collection of interior times.

    theorem lintegral_standardExcursion {Ω : Type} [MeasurableSpace Ω] {P : Measure Ω}
    {B : Fin 3 → ℝ≥0 → Ω → ℝ} (hB : ∀ k,IsPreBrownianReal (B k) P)
    (hI : iIndepFun (fun i ω t => B i t ω) P) {m : ℕ}
    (u : Fin (m+1) → unitInterval) (hu : StrictMono u)
    (h0 : u 0=0) (h1 : ∀ i,(u i:ℝ)<1)
    (F : (Fin m → ℝ) → ℝ≥0∞) (hF : Measurable F) :
    (∫⁻ ω,F (fun i => standardExcursion B ω (u i.succ)) ∂P)=
      ∫⁻ x,F x*bridgeDensity u x := by
…

    Mentions: OAI.FKCRT.standardExcursion, OAI.FKCRT.Radial.bridgeDensity

  49. lemma OAI.FKCRT.Radial.measurable_bridgeDensity line 690