OAI/NumberTheory/TotientAsymptotic/CoordinateCube.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TotientAsymptotic.coordinateCubeShift line 12
2. lemma OAI.TotientAsymptotic.coordinateCubeShift_slack line 16
3. lemma OAI.TotientAsymptotic.coordinateCubeShift_coordinate line 23
4. lemma OAI.TotientAsymptotic.coordinateCubeShift_nonneg line 29
5. lemma OAI.TotientAsymptotic.coordinateCubeShift_budget line 38
6. lemma OAI.TotientAsymptotic.coordinateCubeShift_mem line 44
7. theorem OAI.TotientAsymptotic.coordinate_grid_volume_bound line 62

   Source documentation

   A measurable coordinate event can be counted on the corrected simplex. The pointwise premise will be supplied by the fixed-tolerance band arithmetic.

   theorem coordinate_grid_volume_bound {N : ℕ} (hN : 0<N)
       (B β₀ : ℝ) (β κ : Fin N → ℝ) (K : Finset (Fin N → ℕ))
       (T : Set (Fin N → ℝ)) (hT : MeasurableSet T)
       (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 β₀ β ∧
         ∀ v∈unitGridCell b,simplexScale κ v+coordinateCubeShift N∈T) :
       (K.card:ℝ) ≤ (∏ i,κ i)*
         (volume (prefixRegion N (B+prefixCubeCost N) 0 0 ∩ T)).toReal := by
   …

   Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.unitGridCell, OAI.TotientAsymptotic.enlargedSimplex, OAI.TotientAsymptotic.simplexScale, OAI.TotientAsymptotic.coordinateCubeShift, OAI.TotientAsymptotic.prefixRegion, OAI.TotientAsymptotic.prefixCubeCost