TileStructure.Forest.e728

lemma e728 (hf : BoundedCompactSupport f) (hg : BoundedCompactSupport g) :    ‖∫ x, conj (g x) * (t.boundaryOperator u f x).toReal‖ₑ ≤    ∑ J ∈ 𝓙 (t u), ∫⁻ y in J, ‖f y‖ₑ * maximalFunction volume 𝓑 c𝓑 r𝓑 1 g y *      ∑ I : Grid X, if (J : Set X) ⊆ ball (c I) (16 * D ^ s I) ∧ s J ≤ s I then        (D : ℝ≥0∞) ^ ((s J - s I) / (a : ℝ)) else 0 := by  have nfs := hf.aestronglyMeasurable.enorm  calc    _ = ‖∑ I : Grid X, ((volume (ball (c I) (16 * D ^ s I)))⁻¹.toReal * ∫ x in I, conj (g x)) *        ∑ J ∈ 𝓙' t u (c I) (s I), (D ^ ((s J - s I) / (a : ℝ)) * ∫⁻ y in J, ‖f y‖ₑ).toReal‖ₑ := by      rw [e728_rearrange hf hg]    _ ≤ ∑ I : Grid X, ‖((volume (ball (c I) (16 * D ^ s I)))⁻¹.toReal * ∫ x in I, conj (g x)) *        ∑ J ∈ 𝓙' t u (c I) (s I), (D ^ ((s J - s I) / (a : ℝ)) * ∫⁻ y in J, ‖f y‖ₑ).toReal‖ₑ := by      simp_rw [enorm_eq_nnnorm, ← ENNReal.ofNNReal_finsetSum, ENNReal.coe_le_coe]      apply nnnorm_sum_le    _ ≤ ∑ I : Grid X, (volume (ball (c I) (16 * D ^ s I)))⁻¹ * ‖∫ x in I, conj (g x)‖ₑ *        ∑ J ∈ 𝓙' t u (c I) (s I), ‖(D ^ ((s J - s I) / (a : ℝ)) * ∫⁻ y in J, ‖f y‖ₑ).toReal‖ₑ := by      simp_rw [enorm_mul]; gcongr <;> rw [← ofReal_norm, norm_real, ofReal_norm]      · exact enorm_toReal_le      · simp_rw [enorm_eq_nnnorm, ← ENNReal.ofNNReal_finsetSum, ENNReal.coe_le_coe]        apply nnnorm_sum_le    _ ≤ ∑ I : Grid X, ((volume (ball (c I) (16 * D ^ s I)))⁻¹ * ∫⁻ x in I, ‖g x‖ₑ) *        ∑ J ∈ 𝓙' t u (c I) (s I), D ^ ((s J - s I) / (a : ℝ)) * ∫⁻ y in J, ‖f y‖ₑ := by      gcongr with I      · calc          _ ≤ _ := enorm_integral_le_lintegral_enorm _          _ = _ := by congr! 2 with x; exact RCLike.enorm_conj _      · exact enorm_toReal_le    _ ≤ ∑ I : Grid X,        ((volume (ball (c I) (16 * D ^ s I)))⁻¹ * ∫⁻ x in ball (c I) (16 * D ^ s I), ‖g x‖ₑ) *        ∑ J ∈ 𝓙' t u (c I) (s I), D ^ ((s J - s I) / (a : ℝ)) * ∫⁻ y in J, ‖f y‖ₑ := by      gcongr with I; refine Grid_subset_ball.trans <| ball_subset_ball ?_      exact mul_le_mul_of_nonneg_right (by norm_num) (by positivity)    _ = ∑ I : Grid X, (⨍⁻ x in ball (c I) (16 * D ^ s I), ‖g x‖ₑ ∂volume) *        ∑ J ∈ 𝓙' t u (c I) (s I), D ^ ((s J - s I) / (a : ℝ)) * ∫⁻ y in J, ‖f y‖ₑ := by      congr!; rw [laverage_eq, Measure.restrict_apply .univ, univ_inter, ENNReal.div_eq_inv_mul]    _ = ∑ J ∈ 𝓙 (t u), ∑ I : Grid X, if (J : Set X) ⊆ ball (c I) (16 * D ^ s I) ∧ s J ≤ s I then        (⨍⁻ x in ball (c I) (16 * D ^ s I), ‖g x‖ₑ ∂volume) *          D ^ ((s J - s I) / (a : ℝ)) * ∫⁻ y in J, ‖f y‖ₑ else 0 := by      rw [Finset.sum_comm]; congr with I      simp_rw [Finset.mul_sum, mul_assoc, ← Finset.sum_filter]      refine Finset.sum_congr ?_ fun _ _ ↦ rfl      ext      simp only [𝓙', Finset.mem_filter, Finset.mem_univ, Set.mem_toFinset, true_and]    _ = ∑ J ∈ 𝓙 (t u), ∑ I : Grid X, ∫⁻ y in J,        if (J : Set X) ⊆ ball (c I) (16 * D ^ s I) ∧ s J ≤ s I then          (⨍⁻ x in ball (c I) (16 * D ^ s I), ‖g x‖ₑ ∂volume) *            D ^ ((s J - s I) / (a : ℝ)) * ‖f y‖ₑ else 0 := by      congr!; split_ifs      · rw [lintegral_const_mul'' _ nfs.restrict]      · simp    _ = ∑ J ∈ 𝓙 (t u), ∫⁻ y in J, ∑ I : Grid X,        if (J : Set X) ⊆ ball (c I) (16 * D ^ s I) ∧ s J ≤ s I then          (⨍⁻ x in ball (c I) (16 * D ^ s I), ‖g x‖ₑ ∂volume) *            D ^ ((s J - s I) / (a : ℝ)) * ‖f y‖ₑ else 0 := by      congr with J; refine (lintegral_finsetSum' _ fun I _ ↦ ?_).symm      exact (nfs.restrict.const_mul _).ite (.const _) aemeasurable_const    _ ≤ ∑ J ∈ 𝓙 (t u), ∫⁻ y in J, ∑ I : Grid X,        if (J : Set X) ⊆ ball (c I) (16 * D ^ s I) ∧ s J ≤ s I then          maximalFunction volume 𝓑 c𝓑 r𝓑 1 g y * D ^ ((s J - s I) / (a : ℝ)) * ‖f y‖ₑ else 0 := by      refine Finset.sum_le_sum fun J mJ ↦ setLIntegral_mono_ae ?_ ?_      · refine (Finset.aemeasurable_fun_sum _ fun I _ ↦ ?_).restrict; split_ifs; swap; · simp        refine (AEMeasurable.mul_const ?_ _).mul nfs        exact measurable_maximalFunction.aemeasurable      · refine Eventually.of_forall fun y my ↦ Finset.sum_le_sum fun I _ ↦ ?_        split_ifs with hIJ; swap; · rfl        refine mul_le_mul_left (mul_le_mul_left ?_ _) _        obtain ⟨b, mb, eb⟩ : ∃ i ∈ 𝓑, ball (c𝓑 i) (r𝓑 i) = ball (c I) (16 * D ^ s I) := by          use (4, 0, I); norm_num [𝓑, c𝓑, r𝓑]        rw [maximalFunction]; simp_rw [inv_one, ENNReal.rpow_one]        exact le_iSup₂_of_le b mb (by rw [indicator_of_mem (eb ▸ hIJ.1 my), eb])    _ = _ := by      congr! with J - y -; rw [Finset.mul_sum]      congr with I; rw [mul_ite, mul_zero, ← mul_rotate]