Source indexedlemma · leanprover/lean4:v4.32.0

calculation_5

Carleson.Calculations · Carleson/Calculations.lean:139 to 149

Mathematical statement

Exact Lean statement

lemma calculation_5 {dist_1 dist_2 : ℝ}
    (h : dist_1 ≤ (2 ^ (a : ℝ)) ^ (6 : ℝ) * dist_2) :
    2 ^ ((-𝕔 : ℝ) * a) * dist_1 ≤ 2 ^ ((-(𝕔 - 6) : ℝ) * a) * dist_2

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma calculation_5 {dist_1 dist_2 : ℝ}    (h : dist_1 ≤ (2 ^ (a : ℝ)) ^ (6 : ℝ) * dist_2) :    2 ^ ((-𝕔 : ℝ) * a) * dist_1 ≤ 2 ^ ((-(𝕔 - 6) : ℝ) * a) * dist_2 := by  apply (mul_le_mul_iff_right₀ (show 0 < (2 : ℝ) ^ (𝕔 * (a : ℝ)) by positivity)).mp  rw [← mul_assoc, neg_mul,    Real.rpow_neg (by positivity),    mul_inv_cancel₀ (a := (2 : ℝ) ^ (𝕔 * (a : ℝ))) (by positivity),    ← mul_assoc, ← Real.rpow_add (by positivity)]  ring_nf  rw [Real.rpow_mul (x := (2 : ℝ)) (hx:=by positivity) (y := a) (z := 6)]  exact_mod_cast h