TileStructure.Forest.enorm_adjointCarleson_le_mul_indicator

lemma enorm_adjointCarleson_le_mul_indicator {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‖ₑ) *      (ball (𝔠 p) (8 * D ^ 𝔰 p)).indicator 1 x := by  rw [adjoint_tile_support1, enorm_indicator_eq_indicator_enorm]  calc    _ ≤ (ball (𝔠 p) (5 * D ^ 𝔰 p)).indicator (fun _ ↦        C2_1_3 a * 2 ^ (4 * a) * (volume (ball (𝔠 p) (8 * D ^ 𝔰 p)))⁻¹ *          ∫⁻ y in E p, ‖(𝓘 p : Set X).indicator f y‖ₑ) x := by      gcongr; exact enorm_adjointCarleson_le    _ = C2_1_3 a * 2 ^ (4 * a) * (volume (ball (𝔠 p) (8 * D ^ 𝔰 p)))⁻¹ * (∫⁻ y in E p, ‖f y‖ₑ) *        (ball (𝔠 p) (5 * D ^ 𝔰 p)).indicator 1 x := by      conv_lhs => enter [2, z]; rw [← mul_one (_ * _ * _ * _)]      rw [indicator_const_mul]; congr 2      refine setLIntegral_congr_fun measurableSet_E fun y my ↦ ?_      rw [indicator_of_mem (E_subset_𝓘 my)]    _ ≤ _ := by      gcongr; norm_num