Source indexedlemma · leanprover/lean4:v4.32.0

wiggle_order_11_10

Carleson.TileStructure · Carleson/TileStructure.lean:270 to 281

Source documentation

Lemma 5.3.3, Equation (5.3.3)

Exact Lean statement

lemma wiggle_order_11_10 {n : ℝ} (hp : p ≤ p') (hn : C5_3_3 a ≤ n) : smul n p ≤ smul n p'

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma wiggle_order_11_10 {n : ℝ} (hp : p ≤ p') (hn : C5_3_3 a ≤ n) : smul n p ≤ smul n p' := by  rcases eq_or_ne (𝓘 p) (𝓘 p') with h | h  · rcases eq_or_ne p p' with rfl | h2    · rfl    · exact absurd h (𝓘_strictMono (lt_of_le_of_ne hp h2)).ne  · calc      _ ≤ smul (1 + C2_1_2 a * n) p := by        apply smul_mono_left        rwa [← le_sub_iff_add_le, ← one_sub_mul, ← inv_le_iff_one_le_mul₀']        linarith [C2_1_2_le_inv_256 (X := X)]      _ ≤ smul n p' := smul_C2_1_2 (k := 5⁻¹) n (by norm_num) h        (smul_le_toTileLike.trans <| 𝔓.le_def.mp hp |>.trans toTileLike_le_smul)