Source indexedlemma · leanprover/lean4:v4.32.0

dens₁_le_one

Carleson.TileStructure · Carleson/TileStructure.lean:379 to 395

Source documentation

This density is defined to live in ℝ≥0∞. Use ENNReal.toReal to get a real number. -/ def dens₂ (𝔓' : Set (𝔓 X)) : ℝ≥0∞ := ⨆ (p ∈ 𝔓') (r ≥ 4 * (D ^ 𝔰 p : ℝ)), volume (F ∩ ball (𝔠 p) r) / volume (ball (𝔠 p) r)

lemma le_dens₂ (𝔓' : Set (𝔓 X)) {p : 𝔓 X} (hp : p ∈ 𝔓') {r : ℝ} (hr : r ≥ 4 * (D ^ 𝔰 p : ℝ)) : volume (F ∩ ball (𝔠 p) r) / volume (ball (𝔠 p) r) ≤ dens₂ 𝔓' := le_trans (le_iSup₂ (α := ℝ≥0∞) r hr) (le_iSup₂ p hp)

set_option backward.isDefEq.respectTransparency false in lemma dens₂_eq_biSup_dens₂ (𝔓' : Set (𝔓 X)) : dens₂ (𝔓') = ⨆ (p ∈ 𝔓'), dens₂ ({p}) := by simp [dens₂]

/- A rough estimate. It's also less than 2 ^ (-a)

Exact Lean statement

lemma dens₁_le_one {𝔓' : Set (𝔓 X)} : dens₁ 𝔓' ≤ 1

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma dens₁_le_one {𝔓' : Set (𝔓 X)} : dens₁ 𝔓' ≤ 1 := by  conv_rhs => rw [← mul_one 1]  simp only [dens₁, mem_lowerCubes, iSup_exists, iSup_le_iff]  intros i _ j hj  gcongr  · calc    (j : ℝ≥0∞) ^ (-(a : ℝ)) ≤ 2 ^ (-(a : ℝ)) :=      ENNReal.rpow_le_rpow_of_nonpos (by simp_rw [neg_nonpos, Nat.cast_nonneg'])        (by exact_mod_cast hj)    _ ≤ 2 ^ (0 : ℝ) :=      ENNReal.rpow_le_rpow_of_exponent_le (by norm_num) (neg_nonpos.mpr (Nat.cast_nonneg' _))    _ = 1 := by norm_num  simp only [iSup_le_iff, and_imp]  intros i' _ _ _ _  calc volume (E₂ j i') / volume (𝓘 i' : Set X)  _ ≤ volume (𝓘 i' : Set X) / volume (𝓘 i' : Set X) := by gcongr; apply E₂_subset  _ ≤ 1 := ENNReal.div_self_le_one