Tile.I12_le'

lemma I12_le' {p p' : 𝔓 X} (hle : 𝔰 p' ≤ 𝔰 p) {g : X → ℂ} (x1 : E p') (x2 : E p) :    I12 p p' g x1 x2 ≤    2 ^ ((2 * 𝕔 + 6 + 𝕔 / 4) * a ^ 3 + 8 * a) *      ((1 + edist_{x1.1, D ^ 𝔰 p'} (Q x1) (Q x2)) ^ (-(2 * a ^ 2 + a ^ 3 : ℝ)⁻¹)) /    volume (ball x2.1 (D ^ 𝔰 p)) * ‖g x1‖ₑ * ‖g x2‖ₑ := by  have hD' : 0 < (D : ℝ) ^ 𝔰 p' := defaultD_pow_pos a (𝔰 p')  have hsupp : support (correlation (𝔰 p') (𝔰 p) x1.1 x2) ⊆ ball x1 (D ^ 𝔰 p') :=    fun _ hx ↦ mem_ball_of_correlation_ne_zero hx  -- For compatibility with holder_van_der_corput  have heq : 2 ^ ((2 * 𝕔 + 6 + 𝕔 / 4) * a ^ 3 + 8 * a) *      (1 + edist_{x1.1, D ^ 𝔰 p'} (Q x1) (Q x2)) ^ (-(2 * a ^ 2 + a ^ 3 : ℝ)⁻¹) /      volume (ball x2.1 (D ^ 𝔰 p)) =      (2 ^ ((2 * 𝕔 + 6 + 𝕔 / 4) * a ^ 3 + 8 * a)) / volume (ball x2.1 (D ^ 𝔰 p)) *      (1 + edist_{x1.1, D ^ 𝔰 p'} (Q x1) (Q x2)) ^ (-(2 * a ^ 2 + a ^ 3 : ℝ)⁻¹) := by    rw [ENNReal.mul_comm_div, mul_comm, mul_comm _ (2 ^ _), mul_div_assoc]  simp only [I12, enorm_mul]  gcongr  simp_rw [← sub_eq_neg_add]  apply (holder_van_der_corput hsupp).trans  rw [heq, edist_comm]  gcongr  · have hbdd := correlation_kernel_bound (a := a) (X := X) hle (x₁ := x1) (x₂ := x2)    have hle : C2_0_5 a * volume (ball x1.1 (D ^ 𝔰 p')) *        iHolENorm (correlation (𝔰 p') (𝔰 p) x1.1 x2.1) x1 (2 * D ^ 𝔰 p') τ ≤        C2_0_5 a * volume (ball x1.1 (D ^ 𝔰 p')) *        (C6_2_1 a / (volume (ball x1.1 (D ^ 𝔰 p')) * volume (ball x2.1 (D ^ 𝔰 p)))) := by      gcongr    -- Note: simp, ring_nf, field_simp did not help (because we work with ℝ≥0∞).    have heq : C2_0_5 a * volume (ball x1.1 (D ^ 𝔰 p')) *        (C6_2_1 a / (volume (ball x1.1 (D ^ 𝔰 p')) * volume (ball x2.1 (D ^ 𝔰 p)))) =        C2_0_5 a * (C6_2_1 a / volume (ball x2.1 (D ^ 𝔰 p))) := by      simp only [mul_assoc]      congr 1      rw [ENNReal.div_eq_inv_mul, ENNReal.mul_inv (.inr measure_ball_ne_top)        (.inl measure_ball_ne_top), ← mul_assoc, ← mul_assoc, ENNReal.mul_inv_cancel        (measure_ball_pos volume _ hD').ne' measure_ball_ne_top, one_mul, ENNReal.div_eq_inv_mul]    apply hle.trans    rw [heq, mul_div]    apply ENNReal.div_le_div _ le_rfl    simp only [C2_0_5, C6_2_1, ENNReal.coe_pow, ENNReal.coe_ofNat]    rw [pow_add, mul_comm]    norm_cast    gcongr    · exact one_le_two    · lia