Source indexedlemma · leanprover/lean4:v4.32.0

Tile.uncertainty

Carleson.Antichain.TileCorrelation · Carleson/Antichain/TileCorrelation.lean:293 to 300

Source documentation

Lemma 6.2.3 (edist version).

Exact Lean statement

lemma uncertainty (ha : 1 ≤ a) {p₁ p₂ : 𝔓 X} (hle : 𝔰 p₁ ≤ 𝔰 p₂)
    (hinter : (ball (𝔠 p₁) (5 * D ^ 𝔰 p₁) ∩ ball (𝔠 p₂) (5 * D ^ 𝔰 p₂)).Nonempty) {x₁ x₂ : X}
    (hx₁ : x₁ ∈ E p₁) (hx₂ : x₂ ∈ E p₂) :
    1 + edist_(p₁) (𝒬 p₁) (𝒬 p₂) ≤ C6_2_3 a * (1 + edist_{x₁, D ^ 𝔰 p₁} (Q x₁) (Q x₂))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma uncertainty (ha : 1 ≤ a) {p₁ p₂ : 𝔓 X} (hle : 𝔰 p₁ ≤ 𝔰 p₂)    (hinter : (ball (𝔠 p₁) (5 * D ^ 𝔰 p₁) ∩ ball (𝔠 p₂) (5 * D ^ 𝔰 p₂)).Nonempty) {x₁ x₂ : X}    (hx₁ : x₁ ∈ E p₁) (hx₂ : x₂ ∈ E p₂) :    1 + edist_(p₁) (𝒬 p₁) (𝒬 p₂) ≤ C6_2_3 a * (1 + edist_{x₁, D ^ 𝔰 p₁} (Q x₁) (Q x₂)) := by  have hC : C6_2_3 a = ENNReal.ofReal (C6_2_3 a) := by rw [ENNReal.ofReal_coe_nnreal]  simp only [edist_dist, ← ENNReal.ofReal_one, hC, ← ENNReal.ofReal_add zero_le_one dist_nonneg,    ← ENNReal.ofReal_mul NNReal.zero_le_coe]  exact ENNReal.ofReal_le_ofReal (uncertainty' ha hle hinter hx₁ hx₂)