Source indexedlemma · leanprover/lean4:v4.32.0

exists_le_add_scale_of_mem_maxLayer

Carleson.MinLayerTiles · Carleson/MinLayerTiles.lean:28 to 38

Mathematical statement

Exact Lean statement

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

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma exists_le_add_scale_of_mem_maxLayer (hp : p ∈ A.maxLayer n) :    ∃ p' ∈ A.maxLayer 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_maxLayer_of_le hp (show n ≤ n + 1 by lia)    obtain ⟨q, mq, lq, _⟩ := ih mp'; use q, mq, lp'.trans lq; suffices 𝔰 p < 𝔰 p' by lia    have l : 𝓘 p < 𝓘 p' := by      apply 𝓘_strictMono      exact lt_of_le_of_ne lp' <| (disjoint_maxLayer_of_ne (by lia)).ne_of_mem hp mp'    rw [Grid.lt_def] at l; exact l.2