OAI/Probability/GammaPassage/ActualWitnessScale.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GammaFPP.CrossingBridge.witness_scale_inequalities line 12

   Source documentation

   All three source deterministic inequalities follow from explicit scale cutoffs. The crossing constant is the manuscript's 100(1+|a-|+|a+|).

   lemma witness_scale_inequalities (b m₀ am ap η s L : ℝ) (hm : 0 < m₀)
       (hη : 0 < η) (hη1 : η ≤ 1) (hs : 2 ≤ s)
       (hS : max |m₀-((am+ap)/2)*b| |(am+ap)/2| / η ≤ s)
       (hD : ((η+2*|(am+ap)/2|+1)/m₀)*s ≤ L) :
       max |m₀-((am+ap)/2)*b| |(am+ap)/2| ≤ η*s ∧
       η*s < 2*m₀*L-|(am+ap)/2| *(s+1) ∧
       3*η*s+2*|(am+ap)/2| *(s+1) < 100*(1+|am|+|ap|)*s := by
   …

2. theorem OAI.GammaFPP.CrossingBridge.gamma_witness_scale line 38

   Source documentation

   Construct one genuine characteristic scale satisfying both the deterministic source constraints and actual spatial BK with an explicit entropy parameter.

   theorem gamma_witness_scale (henv : GammaEnvironment shape rate P τ)
       (hshape : 0 < shape) (hrate : 0 < rate) (b η : ℝ)
       (hb : |b| ≤ 1) (hη : 0 < η) (hη1 : η ≤ 1) :
       ∃ k m : ℕ, 2 ≤ (2 : ℝ)^k ∧
         max |(gammaMeanNorm henv hshape hrate) (direction b)-
           ((extremeSlope (gammaMeanNorm henv hshape hrate) b false+extremeSlope (gammaMeanNorm henv hshape hrate) b true)/2)*b|
           |(extremeSlope (gammaMeanNorm henv hshape hrate) b false+extremeSlope (gammaMeanNorm henv hshape hrate) b true)/2| ≤ η*(2 : ℝ)^k ∧
         η*(2 : ℝ)^k < 2*(gammaMeanNorm henv hshape hrate) (direction b)*(2 : ℝ)^m-
           |(extremeSlope (gammaMeanNorm henv hshape hrate) b false+extremeSlope (gammaMeanNorm henv hshape hrate) b true)/2| *((2 : ℝ)^k+1) ∧
         3*η*(2 : ℝ)^k+2*|(extremeSlope (gammaMeanNorm henv hshape hrate) b false+extremeSlope (gammaMeanNorm henv hshape hrate) b true)/2| *((2 : ℝ)^k+1)
           < sourceCrossingK shape rate (gammaMeanNorm henv hshape hrate) b*(2 : ℝ)^k ∧
         ∀ is : List (ℤ×ℤ), P.real {ω | StrictDisjointPaths (spatialListSupport b k m is)
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.gammaMeanNorm, OAI.GammaFPP.CrossingBridge.sourceCrossingK, OAI.GammaFPP.CrossingBridge.spatialListSupport