TileStructure.Forest.holder_correlation_tile_two

lemma holder_correlation_tile_two (hu : u ∈ t) (hp : p ∈ t u) (hf : BoundedCompactSupport f)    (hx : x ∈ ball (𝔠 p) (5 * D ^ 𝔰 p)) (hx' : x' ∈ ball (𝔠 p) (5 * D ^ 𝔰 p)) :    edist (exp (.I * 𝒬 u x) * adjointCarleson p f x) (exp (.I * 𝒬 u x') * adjointCarleson p f x') ≤    C7_5_5 a / volume (ball (𝔠 p) (4 * D ^ 𝔰 p)) *      (edist x x' / D ^ 𝔰 p) ^ (a : ℝ)⁻¹ * ∫⁻ x in E p, ‖f x‖ₑ := by  calc    _ ≤ (∫⁻ y in E p, ‖f y‖ₑ * ‖Ks (𝔰 p) y x‖ₑ * ‖- Q y x + Q y x' + 𝒬 u x - 𝒬 u x'‖ₑ) +        ∫⁻ y in E p, ‖f y‖ₑ * ‖Ks (𝔰 p) y x - Ks (𝔰 p) y x'‖ₑ := holder_correlation_rearrange hf    _ ≤ (∫⁻ y in E p, ‖f y‖ₑ *          (C2_1_3 a / volume (ball y (D ^ 𝔰 p))) * (Q7_5_5 a * (edist x x' / D ^ 𝔰 p) ^ (a : ℝ)⁻¹)) +        ∫⁻ y in E p, ‖f y‖ₑ *          (D2_1_3 a / volume (ball y (D ^ 𝔰 p)) * (edist x x' / D ^ 𝔰 p) ^ (a : ℝ)⁻¹) := by      refine add_le_add (setLIntegral_mono' measurableSet_E fun y my ↦ ?_)        (lintegral_mono fun _ ↦ ?_)      · exact mul_le_mul' (mul_le_mul_right enorm_Ks_le _) (QQQQ_bound my hu hp hx hx')      · gcongr; exact enorm_Ks_sub_Ks_le    _ = (C2_1_3 a * Q7_5_5 a + D2_1_3 a) * (edist x x' / D ^ 𝔰 p) ^ (a : ℝ)⁻¹ *        ∫⁻ y in E p, ‖f y‖ₑ / volume (ball y (D ^ 𝔰 p)) := by      conv_lhs =>        enter [1, 2, y]        rw [← mul_div_assoc, mul_comm ‖f y‖ₑ, mul_div_assoc, ← mul_rotate]      have nt₀ : (edist x x' / D ^ 𝔰 p) ^ (a : ℝ)⁻¹ < ⊤ := by        apply ENNReal.rpow_lt_top_of_nonneg (by positivity); rw [← lt_top_iff_ne_top]        exact ENNReal.div_lt_top (edist_ne_top _ _) (ENNReal.zpow_pos (by simp) (by simp) _).ne'      have nt₁ : Q7_5_5 a * (edist x x' / D ^ 𝔰 p) ^ (a : ℝ)⁻¹ * C2_1_3 a ≠ ⊤ := by finiteness      rw [lintegral_const_mul' _ _ nt₁]      conv_lhs =>        enter [2, 2, y]        rw [← mul_assoc, ← mul_div_assoc, mul_comm ‖f y‖ₑ, mul_div_assoc, ← mul_rotate]      have nt₂ : (edist x x' / D ^ 𝔰 p) ^ (a : ℝ)⁻¹ * D2_1_3 a ≠ ⊤ := by finiteness      rw [lintegral_const_mul' _ _ nt₂, ← add_mul]; congr 1      rw [← mul_rotate, mul_comm _ (D2_1_3 a : ℝ≥0∞), ← add_mul]    _ ≤ (C2_1_3 a * Q7_5_5 a + D2_1_3 a) * (edist x x' / D ^ 𝔰 p) ^ (a : ℝ)⁻¹ *        ∫⁻ y in E p, ‖f y‖ₑ / (volume (ball (𝔠 p) (4 * D ^ 𝔰 p)) / 2 ^ (3 * a)) := by      refine mul_le_mul_right (setLIntegral_mono' measurableSet_E fun y my ↦ ?_) _      exact ENNReal.div_le_div_left (volume_xDsp_bound (E_subset_𝓘 my)) _    _ = 2 ^ (3 * a) * (C2_1_3 a * Q7_5_5 a + D2_1_3 a) / volume (ball (𝔠 p) (4 * D ^ 𝔰 p)) *        (edist x x' / D ^ 𝔰 p) ^ (a : ℝ)⁻¹ * ∫⁻ y in E p, ‖f y‖ₑ := by      conv_lhs =>        enter [2, 2, y]        rw [ENNReal.div_eq_inv_mul]      rw [lintegral_const_mul'' _ hf.restrict.aestronglyMeasurable.enorm, ← mul_assoc]; congr 1      rw [ENNReal.inv_div (by simp) (by simp), ← mul_rotate, ENNReal.mul_div_right_comm]    _ ≤ _ := by      gcongr; rw [C2_1_3, D2_1_3, C7_5_5, Q7_5_5]; norm_cast      calc        _ ≤ 2 ^ (3 * a) * (2 ^ ((𝕔 + 2) * a ^ 3) * (2 ^ 4 * 2 ^ (6 * a))              + 2 ^ ((𝕔 + 2 + 𝕔 / 4) * a ^ 3)) := by gcongr; norm_num        _ ≤ 2 ^ (3 * a) * (2 ^ ((𝕔 + 2 + 𝕔 / 4) * a ^ 3) + 2 ^ ((𝕔 + 2 + 𝕔 / 4) * a ^ 3)) := by          gcongr; rw [← pow_add, ← pow_add]; apply pow_le_pow_right' one_le_two          calc            _ = (𝕔 + 2) * a ^ 3 + 2 * 1 * 2 + 2 * 3 * a := by ring            _ ≤ (𝕔 + 2) * a ^ 3 + 2 * a * a + 2 * a * a := by gcongr <;> linarith [four_le_a X]            _ = (𝕔 + 2) * a ^ 3 + 1 * 4 * a ^ 2 := by ring            _ ≤ (𝕔 + 2) * a ^ 3 + (𝕔 / 4) * a * a ^ 2 := by              gcongr              · have := seven_le_c; lia              · exact four_le_a X            _ = _ := by ring        _ = 2 ^ ((𝕔 + 2 + 𝕔 / 4) * a ^ 3 + (3 * a + 1)) := by          rw [← two_mul, ← pow_succ', ← pow_add]; ring        _ ≤ _ := by          apply pow_le_pow_right' one_le_two          rw [show (𝕔 + 3 + 𝕔 / 4) * a ^ 3 = (𝕔 + 2 + 𝕔 / 4) * a ^ 3 + a ^ 3 by ring]; gcongr          calc            _ = 3 * a * 1 + 1 * 1 * 1 := by ring            _ ≤ 3 * a * a + 1 * a * a := by gcongr <;> linarith [four_le_a X]            _ = 4 * a * a := by ring            _ ≤ _ := by rw [pow_succ, sq]; gcongr; exact four_le_a X