The lower bound Φ ≤ c₂

The period cell cell = [-hgap, hgap) × [-vgap/2, vgap/2) minus the four open slots is goodSet; it has area at least 2 hgap vgap - 4 slotW slotH, and every point of it has a level-one witness using atoms of the neighbouring cells (exists_isWitness_of_abs). The (2N + 1)² translates goodCopy k l, |k|, |l| ≤ N, are disjoint and lie in the level set of smeared N ε at height 1 - 2ε, while ‖smeared N ε‖₁ ≤ (2N + 3)² (1 + heavy). With ε = 1 / (2N + 3) a weak type bound C therefore satisfies C ≥ ((2N + 1)/(2N + 3))³ Φ, and N → ∞ gives C ≥ Φ.

def LeanPool.CenteredMaximal.Lattice.cell : Set (Fin 2 → ℝ)

The period cell [-hgap, hgap) × [-vgap/2, vgap/2).

Equations

• One or more equations did not get rendered due to their size.

def LeanPool.CenteredMaximal.Lattice.slots : Set (Fin 2 → ℝ)

The four open slots, one in each quadrant, excluded from the witnessed region.

Equations

• One or more equations did not get rendered due to their size.

def LeanPool.CenteredMaximal.Lattice.goodSet : Set (Fin 2 → ℝ)

The witnessed part of the period cell.

Equations

• LeanPool.CenteredMaximal.Lattice.goodSet = LeanPool.CenteredMaximal.Lattice.cell \ LeanPool.CenteredMaximal.Lattice.slots

noncomputable def LeanPool.CenteredMaximal.Lattice.shift (k l : ℤ) : Fin 2 → ℝ

The period vector of the cell with index (k, l).

Equations

• LeanPool.CenteredMaximal.Lattice.shift k l = ![2 * ↑k * LeanPool.CenteredMaximal.Lattice.hgap, ↑l * LeanPool.CenteredMaximal.Lattice.vgap]

def LeanPool.CenteredMaximal.Lattice.goodCopy (k l : ℤ) : Set (Fin 2 → ℝ)

The translate of goodSet into the cell with index (k, l).

Equations

• LeanPool.CenteredMaximal.Lattice.goodCopy k l = (fun (z : Fin 2 → ℝ) => -LeanPool.CenteredMaximal.Lattice.shift k l + z) ⁻¹' LeanPool.CenteredMaximal.Lattice.goodSet

theorem LeanPool.CenteredMaximal.Lattice.mem_cell {z : Fin 2 → ℝ} : z ∈ cell ↔ (-hgap ≤ z 0 ∧ z 0 < hgap) ∧ -(vgap / 2) ≤ z 1 ∧ z 1 < vgap / 2

theorem LeanPool.CenteredMaximal.Lattice.measurableSet_slots : MeasurableSet slots

theorem LeanPool.CenteredMaximal.Lattice.measurableSet_goodSet : MeasurableSet goodSet

theorem LeanPool.CenteredMaximal.Lattice.volume_cell : MeasureTheory.volume cell = ENNReal.ofReal (2 * hgap * vgap)

theorem LeanPool.CenteredMaximal.Lattice.volume_slots_le : MeasureTheory.volume slots ≤ (ENNReal.ofReal slotW + ENNReal.ofReal slotW) * (ENNReal.ofReal slotH + ENNReal.ofReal slotH)

The four open slots, each a slotW × slotH rectangle, have total area at most 4 slotW slotH, written in ℝ≥0∞ as (slotW + slotW) * (slotH + slotH).

theorem LeanPool.CenteredMaximal.Lattice.ofReal_le_volume_goodSet : ENNReal.ofReal (2 * hgap * vgap - 4 * (slotW * slotH)) ≤ MeasureTheory.volume goodSet

The witnessed part goodSet = cell \ slots of the period cell has area at least 2 hgap vgap - 4 slotW slotH: the area of cell (volume_cell) minus the bound volume_slots_le on the four slots.

theorem LeanPool.CenteredMaximal.Lattice.volume_goodCopy (k l : ℤ) : MeasureTheory.volume (goodCopy k l) = MeasureTheory.volume goodSet

theorem LeanPool.CenteredMaximal.Lattice.measurableSet_goodCopy (k l : ℤ) : MeasurableSet (goodCopy k l)

theorem LeanPool.CenteredMaximal.Lattice.mem_goodCopy {k l : ℤ} {z : Fin 2 → ℝ} : z ∈ goodCopy k l ↔ ![z 0 - 2 * ↑k * hgap, z 1 - ↑l * vgap] ∈ goodSet

theorem LeanPool.CenteredMaximal.Lattice.pairwiseDisjoint_goodCopy : Set.univ.PairwiseDisjoint fun (p : ℤ × ℤ) => goodCopy p.1 p.2

The translates goodCopy k l, (k, l) : ℤ × ℤ, of goodSet are pairwise disjoint. The index set is all of ℤ × ℤ: restrict it to a finite box with Set.PairwiseDisjoint.subset before adding up volumes with measure_biUnion_finset, as ofReal_le_volume_levelSet does.

theorem LeanPool.CenteredMaximal.Lattice.exists_isWitness_of_mem_goodCopy {k l : ℤ} {z : Fin 2 → ℝ} (hz : z ∈ goodCopy k l) : ∃ (L : ℝ), ∃ A ⊆ nearBox k l, IsWitness (z 0) (z 1) L A

Every point z of the translate goodCopy k l has a level-one witness (L, A) whose atoms lie in nearBox k l. This is exists_isWitness_of_abs (the cell centred at the origin) moved to the cell with index (k, l); nearBox_subset_atomBox then puts the atoms inside atomBox N when |k|, |l| ≤ N, as in ofReal_le_volume_levelSet.

theorem LeanPool.CenteredMaximal.Lattice.nearBox_subset_atomBox {N : ℕ} {k l : ℤ} (hk : |k| ≤ ↑N) (hl : |l| ≤ ↑N) : nearBox k l ⊆ atomBox N

For |k|, |l| ≤ N, the atoms nearBox k l available to a witness in the cell with index (k, l) are kept in atomBox N: the columns 2k - 2, …, 2k + 2 lie in -2N - 2, …, 2N + 2 and the rows l - 1, …, l + 1 lie in -N - 1, …, N + 1.

theorem LeanPool.CenteredMaximal.Lattice.ofReal_le_volume_levelSet (N : ℕ) {ε : ℝ} (hε : 0 < ε) : ENNReal.ofReal ((2 * ↑N + 1) ^ 2 * (2 * hgap * vgap - 4 * (slotW * slotH))) ≤ MeasureTheory.volume {z : Fin 2 → ℝ | ENNReal.ofReal (1 - 2 * ε) < maximalFunction (smeared N ε) z}

The level set of smeared N ε at height 1 - 2ε has measure at least (2N + 1)² times the lower bound 2 hgap vgap - 4 slotW slotH on the area of goodSet (ofReal_le_volume_goodSet), for every ε > 0: it contains the (2N + 1)² disjoint copies goodCopy k l, |k|, |l| ≤ N, of goodSet. This is the level-set side of the weak type inequality in ofReal_mul_phi_le.

theorem LeanPool.CenteredMaximal.Lattice.ofReal_mul_phi_le {C : ENNReal} (hC : IsWeakTypeBound 2 C) (N : ℕ) : ENNReal.ofReal (((2 * ↑N + 1) / (2 * ↑N + 3)) ^ 3 * phi) ≤ C

A weak type bound in dimension two is at least ((2N + 1)/(2N + 3))³ Φ, for every N. This is the finite-N form of ofReal_phi_le, which lets N → ∞.

theorem LeanPool.CenteredMaximal.Lattice.ofReal_phi_le {C : ENNReal} (hC : IsWeakTypeBound 2 C) : ENNReal.ofReal phi ≤ C

Every weak type bound in dimension two is at least Φ. Taking the infimum over all such C with le_weakTypeConstant gives Φ ≤ c₂; ofReal_mul_phi_le is the weaker bound ((2N + 1)/(2N + 3))³ Φ ≤ C for a single N.