OAI/Probability/FKMaps/ExcursionKernel.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FKCRT.Histogram.cube line 11
2. lemma OAI.FKCRT.Histogram.measurableSet_cube line 13
3. lemma OAI.FKCRT.Histogram.volume_cube line 16
4. lemma OAI.FKCRT.Histogram.mem_cube_dist line 21
5. def OAI.FKCRT.Histogram.boxLaw line 28
6. lemma OAI.FKCRT.Histogram.boxLaw_probability line 31
7. lemma OAI.FKCRT.Histogram.boxLaw_dist line 38
8. lemma OAI.FKCRT.Histogram.boxLaw_withDensity line 44
9. def OAI.FKCRT.Histogram.mixture line 61
10. lemma OAI.FKCRT.Histogram.mixture_probability line 64
11. def OAI.FKCRT.Histogram.density line 73
12. lemma OAI.FKCRT.Histogram.measurable_density line 78
13. lemma OAI.FKCRT.Histogram.mixture_withDensity line 85
14. lemma OAI.FKCRT.Histogram.integral_mixture line 101
15. lemma OAI.FKCRT.Histogram.box_integral_lipschitz line 110
16. lemma OAI.FKCRT.Histogram.integral_mixture_close line 124
17. lemma OAI.FKCRT.Histogram.mem_lattice_cube line 154
18. lemma OAI.FKCRT.Histogram.density_lattice line 174
19. lemma OAI.FKCRT.Histogram.density_lattice_negative line 190
20. lemma OAI.FKCRT.Histogram.floor_mesh_tendsto line 203
21. def OAI.FKCRT.SimpleWalk.located line 227
22. def OAI.FKCRT.SimpleWalk.observed line 231
23. lemma OAI.FKCRT.SimpleWalk.tracePoints_observed line 234
24. lemma OAI.FKCRT.SimpleWalk.pathMass_firstHit_observed line 251
25. lemma OAI.FKCRT.SimpleWalk.traceSize_eq_sum line 259
26. lemma OAI.FKCRT.SimpleWalk.pathSum_cast line 265
27. lemma OAI.FKCRT.SimpleWalk.pathMass_cast line 270
28. def OAI.FKCRT.SimpleWalk.evenGrid line 285

    Source documentation

    Even grid time immediately below t, for the odd duration 2n+1.

    def evenGrid (n : ℕ) (t : ℝ) : ℕ := 2*⌊((2*n+1:ℕ):ℝ)*t/2⌋₊

29. lemma OAI.FKCRT.SimpleWalk.even_evenGrid line 287
30. lemma OAI.FKCRT.SimpleWalk.evenGrid_mono line 289
31. lemma OAI.FKCRT.SimpleWalk.evenGrid_zero line 294
32. lemma OAI.FKCRT.SimpleWalk.evenGrid_le line 296
33. lemma OAI.FKCRT.SimpleWalk.evenGrid_error line 305
34. lemma OAI.FKCRT.SimpleWalk.evenGrid_ratio line 315
35. def OAI.FKCRT.SimpleWalk.gridDurations line 335

    Source documentation

    Successive durations at a deterministic increasing list of observation times.

    def gridDurations {m : ℕ} (u : Fin (m+1) → unitInterval) (n : ℕ) (i : Fin m) : ℕ :=
    …

36. def OAI.FKCRT.SimpleWalk.gridRemainder line 338
37. lemma OAI.FKCRT.SimpleWalk.gridDurations_even line 341
38. lemma OAI.FKCRT.SimpleWalk.gridRemainder_even line 346
39. lemma OAI.FKCRT.SimpleWalk.gridDurations_ratio line 351
40. def OAI.FKCRT.SimpleWalk.heat line 373

    Source documentation

    The heat density for one-dimensional standard Brownian motion.

    def heat (t x : ℝ) : ℝ := Real.exp (-x^2/(2*t))/Real.sqrt (2*Real.pi*t)

41. lemma OAI.FKCRT.SimpleWalk.heat_pos line 375
42. lemma OAI.FKCRT.SimpleWalk.heat_continuousOn line 378
43. theorem OAI.FKCRT.SimpleWalk.kernel_uniform_local_limit line 388

    Source documentation

    Full span-two uniform local limit, now for the explicitly reflected simple kernel.

    theorem kernel_uniform_local_limit :
        ∃ E : ℕ → ℝ, (∀ n,0≤E n) ∧ Tendsto E atTop (𝓝 0) ∧
          ∀ (N : ℕ), 0<N → ∀ z : ℤ, Even ((N:ℤ)+z) →
            |Real.sqrt N*kernel N z-(Real.sqrt (2*Real.pi)/Real.pi)*
              Real.exp (-((z:ℝ)/Real.sqrt N)^2/2)|≤E N := by
    …

    Mentions: OAI.FKCRT.SimpleWalk.kernel

44. lemma OAI.FKCRT.SimpleWalk.kernel_local_limit line 404
45. lemma OAI.FKCRT.SimpleWalk.sqrt_ratio_tendsto line 427
46. theorem OAI.FKCRT.SimpleWalk.kernel_scaled_limit line 433

    Source documentation

    Kernel limit at arbitrary macroscopic times and spatial lattice sites.

    theorem kernel_scaled_limit {N T : ℕ → ℕ} {z : ℕ → ℤ} {t x : ℝ}
        (ht : 0<t) (hN : Tendsto N atTop atTop) (hT : Tendsto T atTop atTop)
        (hr : Tendsto (fun n => (N n:ℝ)/(T n:ℝ)) atTop (𝓝 t))
        (hz : ∀ᶠ n in atTop,Even ((N n:ℤ)+z n))
        (hx : Tendsto (fun n => (z n:ℝ)/Real.sqrt (T n:ℝ)) atTop (𝓝 x)) :
        Tendsto (fun n => Real.sqrt (T n:ℝ)*kernel (N n) (z n)) atTop (𝓝 (2*heat t x)) := by
    …

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

47. lemma OAI.FKCRT.SimpleWalk.cast_div_sqrt_tendsto_zero line 474
48. def OAI.FKCRT.SimpleWalk.killedHeat line 479

    Source documentation

    The killed heat kernel obtained from the proved discrete reflection principle.

    def killedHeat (t x y : ℝ) : ℝ := heat t (y-x)-heat t (y+x)

    Mentions: OAI.FKCRT.SimpleWalk.heat

49. lemma OAI.FKCRT.SimpleWalk.killed_scaled_limit line 481
50. lemma OAI.FKCRT.SimpleWalk.sqrt_div_nat_tendsto_zero line 504
51. lemma OAI.FKCRT.SimpleWalk.entrance_scaled_limit line 514
52. lemma OAI.FKCRT.SimpleWalk.firstHit_scaled_limit line 547

    Source documentation

    Terminal first-hitting density at macroscopic time.

    lemma firstHit_scaled_limit {N T b : ℕ → ℕ} {t y : ℝ}
        (ht : 0<t) (hN : Tendsto N atTop atTop) (hT : Tendsto T atTop atTop)
        (hr : Tendsto (fun n => ((N n:ℝ)+1)/(T n:ℝ)) atTop (𝓝 t))
        (hz : ∀ᶠ n in atTop,Even (((N n+1:ℕ):ℤ)+((b n:ℤ)+1)))
        (hy : Tendsto (fun n => (b n:ℝ)/Real.sqrt (T n:ℝ)) atTop (𝓝 y)) :
        Tendsto (fun n => (T n:ℝ)*pathMass (N n+1) (firstHit (b n))) atTop
          (𝓝 (2*y/t*heat t y)) := by
    …

    Mentions: OAI.FKCRT.SimpleWalk.pathMass, OAI.FKCRT.SimpleWalk.firstHit, OAI.FKCRT.SimpleWalk.heat