LogCellBound.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.AffineBernstein.logarithmicBox_subset_unitCells line 22
Source comment
Closed unit cells in the actual logarithmic base coordinates. A fixed logarithmic box is covered by `(2R+1)^k` translated unit cells, including its boundary and the zero-dimensional endpoint.
```
lemma logarithmicBox_subset_unitCells (k R : ℕ) :
    logarithmicBox k R ⊆ ⋃ q : Fin k → Fin (2*R+1),
      logarithmicUnitCell k (fun i => ((q i).val : ℤ)-(R:ℤ)) := by
…
```
Mentions: OAI.AffineBernstein.logarithmicBox, OAI.AffineBernstein.logarithmicUnitCell
theorem OAI.AffineBernstein.measure_logarithmicBox_bound_of_unitCells line 43
Source comment
Uniform nonnegative cell mass implies the exact polynomial box growth used by the source contradiction. No simultaneous large-box convergence is required: only finitely many cell estimates are used for each fixed box.
```
theorem measure_logarithmicBox_bound_of_unitCells {k R : ℕ} (μ : Measure (Space k))
    {C : ℝ≥0∞} (_hC : C ≠ ⊤)
    (hcell : ∀ q : Fin k → Fin (2*R+1),
      μ (logarithmicUnitCell k (fun i => ((q i).val : ℤ)-(R:ℤ))) ≤ C) :
    μ (logarithmicBox k R) ≤ ((2*R+1:ℕ):ℝ≥0∞)^k*C := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.logarithmicUnitCell, OAI.AffineBernstein.logarithmicBox
theorem OAI.AffineBernstein.eventual_logarithmicBox_bound_of_unitCells line 60
Source comment
Pointwise-eventual cell bounds are sufficient for uniformly polynomial box mass; the threshold may depend on the box, just as in the manuscript.
```
theorem eventual_logarithmicBox_bound_of_unitCells {k : ℕ} (μ : ℕ → Measure (Space k))
    {C : ℝ} (hC : 0 ≤ C)
    (hcell : ∀ z : Fin k → ℤ, ∀ᶠ j in atTop,
      μ j (logarithmicUnitCell k z) ≤ ENNReal.ofReal C) (R : ℕ) :
    ∀ᶠ j in atTop, (μ j).real (logarithmicBox k R) ≤ (2^k*C)*(R+1:ℝ)^k := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.logarithmicUnitCell, OAI.AffineBernstein.logarithmicBox