Source indexedlemma · leanprover/lean4:v4.32.0

volume_E₂_le_dens₁_mul_volume

Carleson.TileStructure · Carleson/TileStructure.lean:397 to 406

Mathematical statement

Exact Lean statement

lemma volume_E₂_le_dens₁_mul_volume {𝔓' : Set (𝔓 X)} (mp : p ∈ lowerCubes 𝔓') (mp' : p' ∈ 𝔓')
    {l : ℝ≥0} (hl : 2 ≤ l) (sp : smul l p' ≤ smul l p) :
    volume (E₂ l p) ≤ l ^ a * dens₁ 𝔓' * volume (𝓘 p : Set X)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma volume_E₂_le_dens₁_mul_volume {𝔓' : Set (𝔓 X)} (mp : p ∈ lowerCubes 𝔓') (mp' : p' ∈ 𝔓')    {l : ℝ≥0} (hl : 2 ≤ l) (sp : smul l p' ≤ smul l p) :    volume (E₂ l p) ≤ l ^ a * dens₁ 𝔓' * volume (𝓘 p : Set X) := by  have vpos : volume (𝓘 p : Set X) ≠ 0 := (volume_coeGrid_pos (defaultD_pos a)).ne'  rw [← ENNReal.div_le_iff_le_mul (.inl vpos) (.inl volume_coeGrid_lt_top.ne),    ← ENNReal.rpow_natCast, ← neg_neg (a : ℝ), ENNReal.rpow_neg, ← ENNReal.div_eq_inv_mul]  have plt : (l : ℝ≥0∞) ^ (-(a : ℝ)) ≠ ⊤ := by finiteness  rw [ENNReal.le_div_iff_mul_le (by simp) (.inl plt), mul_comm, dens₁]  refine le_iSup₂_of_le p' mp' (le_iSup₂_of_le l hl ?_); gcongr  exact le_iSup₂_of_le p mp (le_iSup_of_le sp le_rfl)