WitnessBorelCantelli.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.GammaFPP.CrossingBridge.entropy_geometric_bound line 12

Source documentation

Group the floor exponent by its remainder modulo 16.

lemma entropy_geometric_bound (a r : ℝ) (ha : 0 ≤ a) (hr : 0 < r) (hr1 : r ≤ 1) (N : ℕ) :
    a^N*(r^16)^(N/16) ≤ (r^15)⁻¹*(a*r)^N := by
…

theorem OAI.GammaFPP.CrossingBridge.summable_witness_entropy line 29

Source documentation

The exact entropy bound is summable whenever p=r^16 and 196r<1.

theorem summable_witness_entropy (r : ℝ) (hr : 0 < r) (hr1 : r ≤ 1) (hsmall : 196*r < 1) :
    Summable (fun N : ℕ => (196 : ℝ)^N*(r^16)^(N/16)) := by
…

theorem OAI.GammaFPP.CrossingBridge.ae_eventually_spatial_long_paths line 39

Source documentation

Source wi:long-paths at a fixed scale. The same almost-sure event controls all finite simple paths, rather than a single path chosen in advance.

theorem ae_eventually_spatial_long_paths (henv : GammaEnvironment shape rate P τ)
    (hshape : 0 < shape) (hrate : 0 < rate)
    (b m₀ am ap K η r : ℝ) (hb : |b| ≤ 1) (ha : am ≤ ap) (hη : 0 < η)
    (hr : 0 < r) (hr1 : r ≤ 1) (hsmall : 196*r < 1)
    (hgap : 4*η ≤ (ap-am)/2) (k m : ℕ) (hs : 2 ≤ (2 : ℝ)^k)
    (hstep : max |m₀-((am+ap)/2)*b| |(am+ap)/2| ≤ η*(2 : ℝ)^k)
    (hscale₁ : η*(2 : ℝ)^k < 2*m₀*(2 : ℝ)^m-|((am+ap)/2)| *((2 : ℝ)^k+1))
    (hscale₂ : 3*η*(2 : ℝ)^k+2*|((am+ap)/2)| *((2 : ℝ)^k+1) < K*(2 : ℝ)^k)
    (hBK : ∀ is : List (ℤ×ℤ), P.real {ω | StrictDisjointPaths (spatialListSupport b k m is)
      (is.map (spatialWitnessFamily b m₀ am ap K η k m)) (fun e => τ e ω)} ≤ (r^16)^is.length) :
    ∀ᵐ ω ∂P, ∀ᶠ N : ℕ in atTop,
      ∀ blocks : List (List Step), ∀ rest : List Step,
…

Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.CrossingBridge.spatialListSupport, OAI.GammaFPP.CrossingBridge.spatialWitnessFamily