norm_Ks_le'

lemma norm_Ks_le' {x y : X} {𝔄 : Set (𝔓 X)} (p : 𝔄) (hxE : x ∈ E ↑p) (hy : Ks (𝔰 p.1) x y ≠ 0) :    ‖Ks (𝔰 p.1) x y‖ₑ ≤ 2 ^ (6 * a + (𝕔 + 1) * a ^ 3) / volume (ball (𝔠 p.1) (8 * D ^ 𝔰 p.1)) := by  have hDpow_pos : 0 < (D : ℝ) ^ 𝔰 p.1 := defaultD_pow_pos ..  have h8Dpow_pos : 0 < 8 * (D : ℝ) ^ 𝔰 p.1 := mul_defaultD_pow_pos _ (by linarith) _  have hdist_cp : dist x (𝔠 p) ≤ 4 * D ^ 𝔰 p.1 := (mem_ball.mp (Grid_subset_ball hxE.1)).le  have h : ‖Ks (𝔰 p.1) x y‖ₑ ≤ 2 ^ a ^ 3 / volume (ball x (D ^ (𝔰 p.1 - 1) / 4)) := by    apply kernel_bound.trans    grw [C_K, ← Nat.cast_pow, NNReal.rpow_natCast, ENNReal.coe_pow, coe_ofNat, vol,      (dist_mem_Icc_of_Ks_ne_zero hy).1]  apply h.trans  rw [zpow_sub₀ (by simp), zpow_one, div_div]  apply (ineq_6_1_7 x p).trans  have ha : 6 * a + (𝕔 + 1) * a ^ 3 = (5 * a + (𝕔 + 1) * a ^ 3) + a := by lia  simp only [div_eq_mul_inv, ge_iff_le]  rw [ha, pow_add _ (5 * a + (𝕔 + 1) * a ^ 3) a, mul_assoc]  gcongr  suffices volume (ball (𝔠 p.1) (8 * D ^ 𝔰 p.1)) ≤ 2 ^ a * volume (ball x (8 * D ^ 𝔰 p.1)) by    grw [← inv_inv (2 ^ a), ← ENNReal.mul_inv (.inl (by simp)) (.inl (by finiteness)),      ENNReal.inv_le_inv, ← ENNReal.div_eq_inv_mul, ENNReal.div_le_of_le_mul' this]  have h2 : dist x (𝔠 p) + 8 * D ^ 𝔰 p.1 ≤ 2 * (8 * D ^ 𝔰 p.1) :=    calc      _ ≤ (4 : ℝ) * D ^ 𝔰 p.1 + 8 * D ^ 𝔰 p.1 := (add_le_add_iff_right _).mpr hdist_cp      _ ≤ _ := by linarith  convert measure_ball_le_of_dist_le' (μ := volume) zero_lt_two h2  simp [As]