GridMeasure.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem310.gridBadCenters line 13
Source documentation
Centers whose positive displacement of length δ crosses a boundary of the periodic grid with q cells.
```
def gridBadCenters (q : ℕ) (δ : ℝ) : Set ℝ :=
…
```
theorem OAI.Problem310.mem_gridBadCenters_iff line 16
theorem OAI.Problem310.measurableSet_gridBadCenters line 25
theorem OAI.Problem310.gridBadCenters_add_one line 31

theorem OAI.Problem310.gridBadCenters_period_subset line 53

Source documentation

Inside a half-open period the bad centers are covered by exactly q intervals of length δ, provided δ is at most one cell width.

theorem gridBadCenters_period_subset (q : ℕ) (hq : 0 < q) {δ : ℝ}
    (hδ : δ ≤ (q : ℝ)⁻¹) :
    gridBadCenters q δ ∩ Ico (0 : ℝ) 1 ⊆
      ⋃ i : Fin q, Ico (((i.val + 1 : ℕ) : ℝ) / q - δ)
        (((i.val + 1 : ℕ) : ℝ) / q) := by
…

Mentions: OAI.Problem310.gridBadCenters

theorem OAI.Problem310.volume_gridBadCenters_period_le line 83

theorem OAI.Problem310.volume_iUnion_gridBadCenters_period_le line 104

Source documentation

The exceptional density for any finite family of stability requirements is bounded by the sum of its grid-width budgets.

theorem volume_iUnion_gridBadCenters_period_le {ι : Type u_ι} [Fintype ι]
    (q : ι → ℕ) (δ : ι → ℝ) (hq : ∀ i, 0 < q i)
    (hδ0 : ∀ i, 0 ≤ δ i) (hδ : ∀ i, δ i ≤ (q i : ℝ)⁻¹) :
    volume ((⋃ i, gridBadCenters (q i) (δ i)) ∩ Icc (0 : ℝ) 1) ≤
      ENNReal.ofReal (∑ i, (q i : ℝ) * δ i) := by
…

Mentions: OAI.Problem310.gridBadCenters