Source indexedlemma · leanprover/lean4:v4.32.0

le_C2_0_2

Carleson.Discrete.MainTheorem · Carleson/Discrete/MainTheorem.lean:21 to 36

Mathematical statement

Exact Lean statement

lemma le_C2_0_2 (ha : 4 ≤ a) {q : ℝ≥0} (hq : q ∈ Ioc 1 2) :
    C5_1_2 a q + C5_1_3 a q ≤ C2_0_2 a q

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma le_C2_0_2 (ha : 4 ≤ a) {q : ℝ≥0} (hq : q ∈ Ioc 1 2) :    C5_1_2 a q + C5_1_3 a q ≤ C2_0_2 a q := by  have h'q : 0 < q - 1 := tsub_pos_of_lt hq.1  simp only [C5_1_2, C5_1_3, C2_0_2, ge_iff_le]  have : (q - 1) ^ 4 ≥ (q - 1) ^ 5 := by    apply pow_le_pow_of_le_one h'q.le ?_ (by norm_num)    rw [tsub_le_iff_left]    convert hq.2    norm_num  grw [this, ← add_div]  gcongr  apply (add_le_pow_two_add_cube ha le_rfl ?_).trans_eq (by ring)  have : 𝕔 / 8 ≤ 𝕔 / 4 := by lia  grw [this]  ring_nf  lia