OAI/RingTheory/DirectFiniteness/HoleNumerics.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KaplanskyCounterexample.FiniteGeometry.hole_numeric_powers line 8
2. lemma OAI.KaplanskyCounterexample.FiniteGeometry.hole_probability_mem line 37
3. lemma OAI.KaplanskyCounterexample.FiniteGeometry.hole_alteration_numeric line 46

   Source documentation

   Explicit finite alteration arithmetic. The three costs refer to the actual pair, four-witness rectangle, and 101-point occupancy event families.

   lemma hole_alteration_numeric {q D N S C B H : ℝ}
       (hq : 12 ≤ q) (hD : q^100 ≤ D) (hN : 0 ≤ N) (hS : 0 ≤ S)
       (hdensity : N ≤ q^72*S)
       (hC : C ≤ D*S*q^2) (hB : B ≤ D^2*N*q^10)
       (hH : H ≤ D^2*N*(q^122)^101) :
       3*N/D^2 ≤ S*(q^73/D^2) -
         (C*2*(q^73/D^2)^2 + B*4*(q^73/D^2)^4 + H*101*(q^73/D^2)^101) := by
   …