Source indexedlemma · leanprover/lean4:v4.32.0

exists_scale_add_le_of_mem_minLayer

Carleson.MinLayerTiles · Carleson/MinLayerTiles.lean:16 to 26

Mathematical statement

Exact Lean statement

lemma exists_scale_add_le_of_mem_minLayer (hp : p ∈ A.minLayer n) :
    ∃ p' ∈ A.minLayer 0, p' ≤ p ∧ 𝔰 p' + n ≤ 𝔰 p

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma exists_scale_add_le_of_mem_minLayer (hp : p ∈ A.minLayer n) :    ∃ p' ∈ A.minLayer 0, p' ≤ p ∧ 𝔰 p' + n ≤ 𝔰 p := by  induction n generalizing p with  | zero => use p, hp, le_rfl, by lia  | succ n ih =>    obtain ⟨p', mp', lp'⟩ := exists_le_in_minLayer_of_le hp (show n ≤ n + 1 by lia)    obtain ⟨q, mq, lq, _⟩ := ih mp'; use q, mq, lq.trans lp'; suffices 𝔰 p' < 𝔰 p by lia    have l : 𝓘 p' < 𝓘 p := by      apply 𝓘_strictMono      exact lt_of_le_of_ne lp' <| (disjoint_minLayer_of_ne (by lia)).ne_of_mem mp' hp    rw [Grid.lt_def] at l; exact l.2