Source indexedlemma · leanprover/lean4:v4.32.0

disjoint_TilesAt_of_ne

Carleson.Discrete.Defs · Carleson/Discrete/Defs.lean:27 to 32

Mathematical statement

Exact Lean statement

lemma disjoint_TilesAt_of_ne {m n : ℕ} (h : m ≠ n) : Disjoint (TilesAt (X := X) m) (TilesAt n)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma disjoint_TilesAt_of_ne {m n : ℕ} (h : m ≠ n) : Disjoint (TilesAt (X := X) m) (TilesAt n) := by  wlog hl : m < n generalizing m n; · exact (this h.symm (by lia)).symm  by_contra! h; rw [not_disjoint_iff] at h; obtain ⟨p, mp₁, mp₂⟩ := h  simp_rw [TilesAt, mem_preimage, 𝓒, mem_sdiff, aux𝓒, mem_setOf] at mp₁ mp₂  apply absurd _ mp₂.2; obtain ⟨j, lj, vj⟩ := mp₁.1; use j, lj; apply lt_of_le_of_lt _ vj  exact mul_le_mul_left (ENNReal.zpow_le_of_le one_le_two (by lia)) _