Tile.correlation_kernel_bound

lemma correlation_kernel_bound {s₁ s₂ : ℤ} {x₁ x₂ : X} (hs : s₁ ≤ s₂) :    iHolENorm (correlation s₁ s₂ x₁ x₂) x₁ (2 * D ^ s₁) τ ≤    C6_2_1 a / (volume (ball x₁ (D ^ s₁)) * volume (ball x₂ (D ^ s₂))) := by  -- 6.2.4  have hφ' (y : X) : ‖correlation s₁ s₂ x₁ x₂ y‖ₑ ≤      (C2_1_3 a) ^ 2 / (volume (ball x₁ (D ^ s₁)) * volume (ball x₂ (D ^ s₂))):= by    simp only [correlation, enorm_mul, RCLike.enorm_conj, pow_two,      ENNReal.mul_div_mul_comm (.inr measure_ball_ne_top) (.inl measure_ball_ne_top)]    exact mul_le_mul' enorm_Ks_le enorm_Ks_le  -- Bound 6.2.6 + 6.2.7  calc    _ ≤ C2_1_3 a ^ 2 / (volume (ball x₁ (D ^ s₁)) * volume (ball x₂ (D ^ s₂))) +        2 ^ ((2 * 𝕔 + 5 + 𝕔 / 4) * a ^ 3) /        (volume (ball x₁ (D ^ s₁)) * volume (ball x₂ (D ^ s₂))) := by      apply add_le_add (iSup₂_le fun x _ ↦ hφ' x)      simp only [ENNReal.mul_iSup, iSup_le_iff]      intro z hz z' hz' hzz'      convert! e625 hzz' hs      rw [ENNReal.ofReal_mul zero_le_two, ENNReal.ofReal_ofNat, ← Real.rpow_intCast,        ← ENNReal.ofReal_rpow_of_pos (realD_pos _), ENNReal.ofReal_natCast,        ENNReal.rpow_intCast]    _ ≤ _ := by      rw [← ENNReal.add_div]      refine ENNReal.div_le_div_right ?_ _      rw [C2_1_3, C6_2_1]      norm_cast      rw [← pow_mul]      apply add_le_pow_two ?_ le_rfl ?_      · ring_nf        lia      · ring_nf        suffices 1 ≤ a ^ 3 by lia        exact one_le_pow₀ (by linarith [four_le_a X])