Smearing the lattice into an integrable function

For ε > 0, truncate the measure to atomBox N. Replace each atom of mass m at p by m ε⁻² times the indicator of the closed square of side ε centred at p. smeared N ε is integrable; its L¹ norm equals the total mass of the kept atoms.

If (L, A) witnesses level one at z and every atom of A is kept, the square of side L + ε centred at z contains the smeared mass of every atom of A, so the maximal function at z is at least L² / (L + ε)² ≥ (1 + ε)⁻² > 1 - 2ε (lt_maximalFunction_smeared). This is the device of Aldaz (2000, Lemma 1.1), adapted to weighted atoms.

noncomputable def LeanPool.CenteredMaximal.Lattice.atom (p : ℤ × ℤ) : Fin 2 → ℝ

The position (c · hgap, r · vgap) of the atom with index (c, r).

Equations

• LeanPool.CenteredMaximal.Lattice.atom p = ![↑p.1 * LeanPool.CenteredMaximal.Lattice.hgap, ↑p.2 * LeanPool.CenteredMaximal.Lattice.vgap]

def LeanPool.CenteredMaximal.Lattice.atomBox (N : ℕ) : Finset (ℤ × ℤ)

The atoms kept at scale N: columns -2N-2, …, 2N+2 and rows -N-1, …, N+1.

Equations

• LeanPool.CenteredMaximal.Lattice.atomBox N = Finset.Icc (-2 * ↑N - 2) (2 * ↑N + 2) ×ˢ Finset.Icc (-↑N - 1) (↑N + 1)

noncomputable def LeanPool.CenteredMaximal.Lattice.smeared (N : ℕ) (ε : ℝ) (z : Fin 2 → ℝ) : ℝ

The truncated lattice with each atom smeared over the closed square of side ε.

Equations

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

theorem LeanPool.CenteredMaximal.Lattice.colWeight_pos (c : ℤ) : 0 < colWeight c

theorem LeanPool.CenteredMaximal.Lattice.smeared_nonneg (N : ℕ) (ε : ℝ) (z : Fin 2 → ℝ) : 0 ≤ smeared N ε z

theorem LeanPool.CenteredMaximal.Lattice.integrable_smeared (N : ℕ) (ε : ℝ) : MeasureTheory.Integrable (smeared N ε) MeasureTheory.volume

theorem LeanPool.CenteredMaximal.Lattice.sum_range_colWeight (m : ℕ) : ∑ n ∈ Finset.range (2 * m + 1), colWeight ↑n = ↑m + 1 + ↑m * heavy

Consecutive columns 0, …, 2m carry mass (m + 1) + m · heavy: the m + 1 even columns have mass 1 and the m odd columns have mass heavy.

theorem LeanPool.CenteredMaximal.Lattice.sum_colWeight_Icc (N : ℕ) : ∑ c ∈ Finset.Icc (-2 * ↑N - 2) (2 * ↑N + 2), colWeight c = 2 * ↑N + 3 + (2 * ↑N + 2) * heavy

The columns -2N - 2, …, 2N + 2 of atomBox N carry total mass (2N + 3) + (2N + 2) · heavy: the 2N + 3 even columns have mass 1 and the 2N + 2 odd columns have mass heavy.

theorem LeanPool.CenteredMaximal.Lattice.sum_colWeight_atomBox (N : ℕ) : ∑ p ∈ atomBox N, colWeight p.1 = (2 * ↑N + 3) * (2 * ↑N + 3 + (2 * ↑N + 2) * heavy)

The atoms of atomBox N carry total mass (2N + 3) · ((2N + 3) + (2N + 2) · heavy): each of its 2N + 3 rows carries the column mass of sum_colWeight_Icc. See sum_colWeight_atomBox_le for the cruder bound (2N + 3)² · (1 + heavy).

theorem LeanPool.CenteredMaximal.Lattice.sum_colWeight_atomBox_le (N : ℕ) : ∑ p ∈ atomBox N, colWeight p.1 ≤ (2 * ↑N + 3) ^ 2 * (1 + heavy)

theorem LeanPool.CenteredMaximal.Lattice.ofReal_mul_indicator_one {s : Set (Fin 2 → ℝ)} (a : ℝ) (z : Fin 2 → ℝ) : ENNReal.ofReal (a * s.indicator 1 z) = s.indicator (fun (x : Fin 2 → ℝ) => ENNReal.ofReal a) z

theorem LeanPool.CenteredMaximal.Lattice.enorm_smeared (N : ℕ) (ε : ℝ) (z : Fin 2 → ℝ) : ‖smeared N ε z‖ₑ = ∑ p ∈ atomBox N, (Metric.closedBall (atom p) (ε / 2)).indicator (fun (x : Fin 2 → ℝ) => ENNReal.ofReal (colWeight p.1 / ε ^ 2)) z

theorem LeanPool.CenteredMaximal.Lattice.ofReal_div_sq_mul_volume {ε : ℝ} (hε : 0 < ε) (p : ℤ × ℤ) : ENNReal.ofReal (colWeight p.1 / ε ^ 2) * MeasureTheory.volume (Metric.closedBall (atom p) (ε / 2)) = ENNReal.ofReal (colWeight p.1)

A smeared atom has integral equal to its mass.

theorem LeanPool.CenteredMaximal.Lattice.lintegral_smeared (N : ℕ) {ε : ℝ} (hε : 0 < ε) : ∫⁻ (z : Fin 2 → ℝ), ‖smeared N ε z‖ₑ = ENNReal.ofReal (∑ p ∈ atomBox N, colWeight p.1)

theorem LeanPool.CenteredMaximal.Lattice.ofReal_sq_le_setLIntegral_smeared {N : ℕ} {ε : ℝ} (hε : 0 < ε) {z : Fin 2 → ℝ} {L : ℝ} {A : Finset (ℤ × ℤ)} (hA : A ⊆ atomBox N) (hw : IsWitness (z 0) (z 1) L A) : ENNReal.ofReal (L ^ 2) ≤ ∫⁻ (y : Fin 2 → ℝ) in Metric.closedBall z ((L + ε) / 2), ‖smeared N ε y‖ₑ

If (L, A) witnesses level one at z and atomBox N keeps every atom of A, then the closed square of side L + ε centred at z (a closedBall in the sup metric) carries smeared mass at least L ^ 2. Unlike lintegral_smeared, which integrates over the whole plane, this bounds the mass inside a single square, as lt_maximalFunction_smeared needs.

theorem LeanPool.CenteredMaximal.Lattice.lt_maximalFunction_smeared {N : ℕ} {ε : ℝ} (hε : 0 < ε) {z : Fin 2 → ℝ} {L : ℝ} {A : Finset (ℤ × ℤ)} (hA : A ⊆ atomBox N) (hw : IsWitness (z 0) (z 1) L A) : ENNReal.ofReal (1 - 2 * ε) < maximalFunction (smeared N ε) z

If (L, A) witnesses level one at z and atomBox N keeps every atom of A, then the maximal function of smeared N ε at z exceeds 1 - 2ε. The bound is uniform in N and in the witness, so it holds at every point that has some witness inside atomBox N. Compare ofReal_sq_le_setLIntegral_smeared, which bounds the mass of the square of side L + ε rather than the maximal function.