TileStructure.Forest.enorm_adjointCarleson_le

lemma enorm_adjointCarleson_le {x : X} :    ‖adjointCarleson p f x‖ₑ ≤    C2_1_3 a * 2 ^ (4 * a) * (volume (ball (𝔠 p) (8 * D ^ 𝔰 p)))⁻¹ * ∫⁻ y in E p, ‖f y‖ₑ := by  calc    _ ≤ ∫⁻ y in E p, ‖conj (Ks (𝔰 p) y x) * exp (.I * (Q y y - Q y x)) * f y‖ₑ := by      apply enorm_integral_le_lintegral_enorm    _ = ∫⁻ y in E p, ‖Ks (𝔰 p) y x‖ₑ * ‖f y‖ₑ := by      congr! with y      rw [enorm_mul, enorm_mul, ← ofReal_sub, enorm_exp_I_mul_ofReal, RCLike.enorm_conj, mul_one]    _ ≤ C2_1_3 a * ∫⁻ y in E p, (volume (ball y (D ^ 𝔰 p)))⁻¹ * ‖f y‖ₑ := by      rw [← lintegral_const_mul' _ _ (by simp)]      refine lintegral_mono fun y ↦ ?_      rw [← mul_assoc, mul_comm _ _⁻¹, ← ENNReal.div_eq_inv_mul]      exact mul_le_mul_left enorm_Ks_le _    _ ≤ _ := by      rw [mul_assoc _ (_ ^ _), mul_comm (_ ^ _), ← ENNReal.div_eq_inv_mul,        ← ENNReal.inv_div (.inl (by simp)) (.inl (by simp)), mul_assoc, ← lintegral_const_mul' _⁻¹]      swap      · simp_rw [ne_eq, ENNReal.inv_eq_top, ENNReal.div_eq_zero_iff, ENNReal.pow_eq_top_iff,          ENNReal.ofNat_ne_top, false_and, or_false]        exact (measure_ball_pos _ _ (by unfold defaultD; positivity)).ne'      refine mul_le_mul_right (setLIntegral_mono' measurableSet_E fun y my ↦ ?_) _      exact mul_le_mul_left (ENNReal.inv_le_inv' (volume_xDsp_bound_4 (E_subset_𝓘 my))) _