OAI/Probability/FKMaps/RadialBridge.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FKCRT.Radial.lintegral_plane line 11

   Source documentation

   Polar integration for an arbitrary nonnegative radial function in a plane.

   lemma lintegral_plane (F : ℝ → ℝ≥0∞) (hF : Measurable F) :
       (∫⁻ p : ℝ×ℝ,F (Real.sqrt (p.1^2+p.2^2)))=
         ENNReal.ofReal (2*Real.pi)*∫⁻ r : ℝ in Ioi 0,ENNReal.ofReal r*F r := by
   …

2. lemma OAI.FKCRT.Radial.sqrt_sum_image line 36
3. lemma OAI.FKCRT.Radial.lintegral_radius_substitution line 57

   Source documentation

   Cylindrical radius substitution with its exact Jacobian.

   lemma lintegral_radius_substitution (x : ℝ) (G : ℝ → ℝ≥0∞) :
       (∫⁻ r : ℝ in Ioi 0,ENNReal.ofReal r*G (Real.sqrt (x^2+r^2)))=
         ∫⁻ s : ℝ in Ioi |x|,ENNReal.ofReal s*G s := by
   …

4. lemma OAI.FKCRT.Radial.lintegral_slice line 92

   Source documentation

   Tonelli over the cylindrical slice |x| < s.

   lemma lintegral_slice (G : ℝ×ℝ → ℝ≥0∞) (hG : Measurable G) :
       (∫⁻ x : ℝ,∫⁻ s : ℝ in Ioi |x|,G (x,s))=
         ∫⁻ s : ℝ in Ioi 0,∫⁻ x : ℝ in Ioo (-s) s,G (x,s) := by
   …

5. theorem OAI.FKCRT.Radial.lintegral_cylindrical line 119

   Source documentation

   Three-dimensional radial integration, disintegrated along the first coordinate. This supplies the radial noncentral-Gaussian transition without assuming a Bessel law.

   theorem lintegral_cylindrical (G : ℝ×ℝ → ℝ≥0∞) (hG : Measurable G) :
       (∫⁻ p : ℝ×(ℝ×ℝ),G (p.1,Real.sqrt (p.1^2+p.2.1^2+p.2.2^2)))=
         ENNReal.ofReal (2*Real.pi)*
           ∫⁻ s : ℝ in Ioi 0,ENNReal.ofReal s*∫⁻ x : ℝ in Ioo (-s) s,G (x,s) := by
   …

6. def OAI.FKCRT.SimpleWalk.radialHeat line 154

   Source documentation

   Radial transition density of three-dimensional Brownian motion.

   def radialHeat (t r s : ℝ) : ℝ :=
   …

7. def OAI.FKCRT.SimpleWalk.cylindricalDensity line 158

   Source documentation

   Gaussian density in cylindrical coordinates, with the axial coordinate remaining.

   def cylindricalDensity (t r s x : ℝ) : ℝ :=
   …

8. lemma OAI.FKCRT.SimpleWalk.cylindricalDensity_continuous line 161
9. lemma OAI.FKCRT.SimpleWalk.cylindricalDensity_nonneg line 166
10. lemma OAI.FKCRT.SimpleWalk.cylindricalDensity_endpoint line 171
11. lemma OAI.FKCRT.SimpleWalk.cylindricalDensity_neg_endpoint line 184
12. lemma OAI.FKCRT.SimpleWalk.integral_exp_linear line 193
13. theorem OAI.FKCRT.SimpleWalk.cylindrical_integral line 205

    Source documentation

    Angular integration gives the reflection-kernel formula, including the entrance r=0.

    theorem cylindrical_integral {t r s : ℝ} (ht : 0<t) (hr : 0≤r) (hs : 0≤ s) :
        2*Real.pi*s*(∫ x : ℝ in Ioo (-s) s,cylindricalDensity t r s x)=radialHeat t r s := by
    …

    Mentions: OAI.FKCRT.SimpleWalk.cylindricalDensity, OAI.FKCRT.SimpleWalk.radialHeat

14. lemma OAI.FKCRT.SimpleWalk.radialHeat_nonneg line 242
15. lemma OAI.FKCRT.SimpleWalk.cylindricalDensity_of_norm line 247
16. theorem OAI.FKCRT.SimpleWalk.lintegral_radial_gaussian line 262

    Source documentation

    Exact radial image of the genuinely shifted three independent Gaussian densities. The formula is a proved change of variables, not a Bessel-process assumption.

    theorem lintegral_radial_gaussian {t r : ℝ} (ht : 0<t) (hr : 0≤r)
        (F : ℝ → ℝ≥0∞) (hF : Measurable F) :
        (∫⁻ p : ℝ×(ℝ×ℝ), ENNReal.ofReal (heat t (p.1-r)*heat t p.2.1*heat t p.2.2)*
          F (Real.sqrt (p.1^2+p.2.1^2+p.2.2^2)))=
          ∫⁻ s : ℝ in Ioi 0,ENNReal.ofReal (radialHeat t r s)*F s := by
    …

    Mentions: OAI.FKCRT.SimpleWalk.heat, OAI.FKCRT.SimpleWalk.radialHeat

17. lemma OAI.FKCRT.SimpleWalk.heat_neg line 295
18. lemma OAI.FKCRT.SimpleWalk.heat_bridge line 298

    Source documentation

    The elementary Gaussian bridge identity with its exact normalizing constants.

    lemma heat_bridge {A B : ℝ} (hB : 0<B) (hBA : B<A) (r s : ℝ) :
        heat ((A-B)*B/A) (s-(B/A)*r)*heat A r=heat (A-B) (s-r)*heat B s := by
    …

    Mentions: OAI.FKCRT.SimpleWalk.heat

19. theorem OAI.FKCRT.SimpleWalk.radialHeat_bridge line 319

    Source documentation

    Gaussian regression and the radial heat transform agree, including radius zero.

    theorem radialHeat_bridge {A B : ℝ} (hB : 0<B) (hBA : B<A) (r s : ℝ) :
        radialHeat ((A-B)*B/A) ((B/A)*r) s=
          radialHeat (A-B) r s*((A/B)*heat B s/heat A r) := by
    …

    Mentions: OAI.FKCRT.SimpleWalk.radialHeat, OAI.FKCRT.SimpleWalk.heat

20. def OAI.FKCRT.SimpleWalk.hitHeat line 362
21. lemma OAI.FKCRT.SimpleWalk.hitHeat_pos line 364
22. lemma OAI.FKCRT.SimpleWalk.conditioned_kernel_limit line 369

    Source documentation

    Positive-radius bridge transition, directly from the reflected kernels and the terminal ballot factor.

    lemma conditioned_kernel_limit {J R T a b : ℕ → ℕ} {s t x y : ℝ}
        (hs : 0<s) (ht : 0<t) (hx : 0<x)
        (hJ : Tendsto J atTop atTop) (hR : Tendsto R atTop atTop)
        (hT : Tendsto T atTop atTop)
        (hrJ : Tendsto (fun n => (J n:ℝ)/(T n:ℝ)) atTop (𝓝 s))
        (hrR : Tendsto (fun n => ((R n:ℝ)+1)/(T n:ℝ)) atTop (𝓝 t))
        (hzJ : ∀ᶠ n in atTop,Even ((J n:ℤ)+(b n:ℤ)-a n))
        (hzR : ∀ᶠ n in atTop,Even (((R n+1:ℕ):ℤ)+((b n:ℤ)+1)))
        (hzA : ∀ᶠ n in atTop,Even (((J n+R n+1:ℕ):ℤ)+((a n:ℤ)+1)))
        (ha : Tendsto (fun n => (a n:ℝ)/Real.sqrt (T n:ℝ)) atTop (𝓝 x))
        (hb : Tendsto (fun n => (b n:ℝ)/Real.sqrt (T n:ℝ)) atTop (𝓝 y)) :
        Tendsto (fun n => Real.sqrt (T n:ℝ)/2*
    …

23. lemma OAI.FKCRT.SimpleWalk.firstHit_zero_scaled_limit line 406
24. lemma OAI.FKCRT.SimpleWalk.entrance_conditioned_limit line 427
25. abbrev OAI.FKCRT.Radial.Space line 478
26. def OAI.FKCRT.Radial.axis line 480
27. def OAI.FKCRT.Radial.step line 482
28. instance OAI.FKCRT.Radial.step_probability line 485
29. lemma OAI.FKCRT.Radial.norm_axis line 489
30. lemma OAI.FKCRT.Radial.gaussian_affine line 495
31. theorem OAI.FKCRT.Radial.step_coordinates line 505

    Source documentation

    The orthogonally invariant Gaussian step is exactly the product of its three coordinates.

    theorem step_coordinates {t : ℝ} (ht : 0≤t) (v : Space) :
        step t v=(Measure.pi (fun i : Fin 3 => gaussianReal (v i) (⟨t,ht⟩ : ℝ≥0))).map (toLp 2) := by
    …

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

32. lemma OAI.FKCRT.Radial.step_rotation line 522
33. lemma OAI.FKCRT.Radial.step_norm_rotation line 532
34. lemma OAI.FKCRT.Radial.step_norm_axis line 539
35. def OAI.FKCRT.Radial.coordinates line 548
36. lemma OAI.FKCRT.Radial.coordinates_apply line 552
37. lemma OAI.FKCRT.Radial.coordinates_symm_apply line 553
38. lemma OAI.FKCRT.Radial.coordinates_preserving line 558
39. lemma OAI.FKCRT.Radial.norm_coordinates line 570
40. lemma OAI.FKCRT.Radial.heat_gaussianPDF line 579
41. theorem OAI.FKCRT.Radial.lintegral_step_norm line 589

    Source documentation

    The norm of a Gaussian step has exactly the derived radial heat-kernel law.

    theorem lintegral_step_norm {t : ℝ} (ht : 0<t) (v : Space)
        (F : ℝ → ℝ≥0∞) (hF : Measurable F) :
        (∫⁻ z,F ‖z‖ ∂step t v)=
          ∫⁻ s : ℝ in Ioi 0,ENNReal.ofReal (radialHeat t ‖v‖ s)*F s := by
    …

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

42. def OAI.FKCRT.Radial.transition line 635

    Source documentation

    Lebesgue density supported on strictly positive radii.

    def transition (t r s : ℝ) : ℝ≥0∞ :=
    …

43. lemma OAI.FKCRT.Radial.measurable_transition line 638
44. lemma OAI.FKCRT.Radial.lintegral_step_transition line 645
45. def OAI.FKCRT.Radial.chain line 653

    Source documentation

    A finite affine Gaussian Markov chain, including a prescribed initial vector.

    def chain : {m : ℕ} → Space → (Fin m → ℝ) → (Fin m → ℝ) → (Fin m → Space) → Fin m → Space
      | 0,_,_,_,_ => Fin.elim0
      | _m+1,v,a,t,z =>
        let w := a 0 • v+Real.sqrt (t 0) • z 0
    …

    Mentions: OAI.FKCRT.Radial.Space

46. lemma OAI.FKCRT.Radial.continuous_chain line 659
47. def OAI.FKCRT.Radial.chainDensity line 675

    Source documentation

    Joint density, in chronological order, for the radii of that chain.

    def chainDensity : {m : ℕ} → ℝ → (Fin m → ℝ) → (Fin m → ℝ) → (Fin m → ℝ) → ℝ≥0∞
      | 0,_,_,_,_ => 1
      | _m+1,r,a,t,x => transition (t 0) (|a 0| *r) (x 0)*
        chainDensity (x 0) (Fin.tail a) (Fin.tail t) (Fin.tail x)

    Mentions: OAI.FKCRT.Radial.transition

48. lemma OAI.FKCRT.Radial.measurable_chainDensity line 680
49. theorem OAI.FKCRT.Radial.lintegral_chain line 695

    Source documentation

    Radial integration for every finite affine Gaussian chain, without invoking an unformalized Bessel process or its transition theorem.

    theorem lintegral_chain (m : ℕ) (v : Space) (a t : Fin m → ℝ)
        (ht : ∀ i,0<t i) (F : (Fin m → ℝ) → ℝ≥0∞) (hF : Measurable F) :
        (∫⁻ z,F (fun i => ‖chain v a t z i‖) ∂Measure.pi (fun _ => stdGaussian Space))=
        ∫⁻ x,F x*chainDensity ‖v‖ a t x := by
    …

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