OAI/NumberTheory/TotientAsymptotic/UnbandedCube.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TotientAsymptotic.prefixCubeCost line 12
2. lemma OAI.TotientAsymptotic.prefixCubeCost_nonneg line 15
3. lemma OAI.TotientAsymptotic.prefixRegion_unit_cube line 19
4. lemma OAI.TotientAsymptotic.simplexScale_unit_distance line 33
5. theorem OAI.TotientAsymptotic.unbanded_grid_volume_bound line 43

   Source documentation

   Diagonal normalization followed by additive cube error does not require lower coordinate bands. The error is the exact renewal-weighted sum.

   theorem unbanded_grid_volume_bound {N : ℕ} (hN : 0 < N)
       (B β₀ : ℝ) (β κ : Fin N → ℝ) (K : Finset (Fin N → ℕ))
       (hB : 0 ≤ B) (hβ₀ : 0 < β₀) (hβ : ∀ i, 0 < β i)
       (hκ : ∀ i, 1 ≤ κ i) (htop : ∀ i, β₀ ≤ κ i)
       (hstep : ∀ i j, i < j → β i*κ i ≤ κ j)
       (hK : ∀ b ∈ K, ∃ u ∈ unitGridCell b, u ∈ enlargedSimplex N B β₀ β) :
       (K.card:ℝ) ≤ (∏ i, κ i)*
         ((B+prefixCubeCost N)^N/((N.factorial:ℝ)*∏ i : Fin N, g (i.val+1))) := by
   …

   Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.unitGridCell, OAI.TotientAsymptotic.enlargedSimplex, OAI.TotientAsymptotic.prefixCubeCost, OAI.TotientAsymptotic.g