TileStructure.Forest.third_tree_pointwise

lemma third_tree_pointwise (hu : u ∈ t) (hL : L ∈ 𝓛 (t u)) (hx : x ∈ L) (hx' : x' ∈ L)    (hf : BoundedCompactSupport f) :    ‖∑ i ∈ t.σ u x, ∫ y, Ks i x y * (f y - approxOnCube (𝓙 (t u)) f y)‖ₑ ≤    C7_1_6 a * t.boundaryOperator u (approxOnCube (𝓙 (t u)) (‖f ·‖)) x' := by  classical  let I (i : ℤ) (x : X) := ‖∫ (y : X), Ks i x y * (f y - approxOnCube (𝓙 (t u)) f y)‖ₑ  let Js (p : 𝔓 X) := Set.toFinset <| { J ∈ 𝓙 (t u) | ↑J ⊆ ball x (16 * D ^ 𝔰 p) ∧ s J ≤ 𝔰 p }  let ps (I : Grid X) := Finset.univ.filter (fun p ↦ p ∈ t u ∧ 𝓘 p = I)  let 𝔗_fin := Finset.univ.filter (· ∈ t u)  have A5_pos : (defaultA a : ℝ) ^ 5 > 0 := pow_pos (by norm_num) 5  calc    _ ≤ ∑ i ∈ t.σ u x, ‖∫ y, Ks i x y * (f y - approxOnCube (𝓙 (t u)) f y)‖ₑ :=      enorm_sum_le (t.σ u x) _    _ = ∑ p ∈ 𝔗_fin, (E p).indicator 1 x * I (𝔰 p) x := by      rw [← p_sum_eq_s_sum I]      simp_rw [indicator_eq_indicator_one_mul _ (I _), 𝔗_fin]    _ ≤ ∑ p ∈ 𝔗_fin, (E p).indicator 1 x *          (D2_1_3 a / (volume (ball x (D ^ 𝔰 p))) * 2 ^ (3 / a : ℝ) *          ∑ J ∈ 𝓙' t u (𝔠 p) (𝔰 p), D ^ ((s J - 𝔰 p) / (a : ℝ)) * ∫⁻ y in J, ‖f y‖ₑ) := by      refine Finset.sum_le_sum fun J hJ ↦ ?_      by_cases xJ : x ∈ E J      · rw [indicator_of_mem xJ, Pi.one_apply, one_mul, one_mul]        exact L7_1_6_I_le hu hf (Finset.mem_filter.mp hJ).2 xJ      · simp only [indicator_of_notMem xJ, zero_mul, le_refl]    _ = ∑ I : Grid X, ∑ p ∈ ps I, (E p).indicator 1 x *          (D2_1_3 a / (volume (ball x (D ^ s I))) * 2 ^ (3 / a : ℝ) *          ∑ J ∈ 𝓙' t u (c I) (s I), D ^ ((s J - s I) / (a : ℝ)) * ∫⁻ y in J, ‖f y‖ₑ) := by      let summand := fun (y : X) (i : ℤ) ↦          D2_1_3 a / volume (ball x (D ^ i)) * 2 ^ (3 / a : ℝ) *          ∑ J ∈ 𝓙' t u y i, D ^ ((s J - (i : ℝ)) / a) * ∫⁻ y in J, ‖f y‖ₑ      exact sum_p_eq_sum_I_sum_p t u x summand    _ ≤ ∑ I : Grid X, ∑ p ∈ ps I, (E p).indicator 1 x *          (D2_1_3 a / (volume (ball (c I) (16 * D ^ s I)) / defaultA a ^ 5) *          2 ^ (3 / a : ℝ) *          ∑ J ∈ 𝓙' t u (c I) (s I), D ^ ((s J - s I) / (a : ℝ)) * ∫⁻ y in J, ‖f y‖ₑ) := by      refine Finset.sum_le_sum fun I _ ↦ Finset.sum_le_sum fun p hp ↦ ?_      by_cases xEp : x ∈ E p; swap      · simp only [indicator_of_notMem xEp, zero_mul, le_refl]      apply mul_le_mul_right      gcongr; apply ENNReal.div_le_of_le_mul'      calc        _ ≤ volume (ball x (32 * D ^ s I)) := by          refine measure_mono (ball_subset_ball' ?_)          suffices dist (c I) x < 4 * D ^ (s I) by linarith [defaultD_pow_pos a (s I)]          exact mem_ball'.mp <| (Finset.mem_filter.mp hp).2.2 ▸ Grid_subset_ball (E_subset_𝓘 xEp)        _ ≤ _ := by          rw [show (32 : ℝ) = 2 ^ 5 by norm_num]          exact measure_ball_two_le_same_iterate x (D ^ s I) 5    _ ≤ ∑ I : Grid X, ((I : Set X).indicator 1 x') *          (D2_1_3 a / (volume (ball (c I) (16 * D ^ s I)) / defaultA a ^ 5) *          2 ^ (3 / a : ℝ) *          ∑ J ∈ 𝓙' t u (c I) (s I), D ^ ((s J - s I) / (a : ℝ)) * ∫⁻ y in J, ‖f y‖ₑ) := by      simp_rw [← Finset.sum_mul]      gcongr with I hI      by_cases! ex : ∃ p ∈ ps I, x ∈ E p      · obtain ⟨p, hp, xEp⟩ := ex        have L_subset_I : (L : Set X) ⊆ (I : Set X) := by          simp only [ps, Finset.mem_filter] at hp          exact hp.2.2 ▸ subset_of_mem_𝓛 hL hp.2.1 (not_disjoint_iff.mpr ⟨x, ⟨E_subset_𝓘 xEp, hx⟩⟩)        simp only [L_subset_I hx', indicator_of_mem, Pi.one_apply]        rw [Finset.sum_eq_single_of_mem p hp]        · exact le_of_eq <| (indicator_eq_one_iff_mem _).mpr xEp        · intro p' hp' p'_ne_p          simp only [ps, Finset.mem_filter] at hp hp'          exact (indicator_eq_zero_iff_notMem _).mpr fun xEp' ↦            disjoint_left.mp (disjoint_Ω p'_ne_p (hp'.2.2.trans hp.2.2.symm)) xEp'.2.1 xEp.2.1      · suffices ∑ p ∈ ps I, (E p).indicator (1 : X → ℝ≥0∞) x = 0 by rw [this]; exact zero_le        exact Finset.sum_eq_zero (fun p hp ↦ indicator_of_notMem (ex p hp) _)    _ = ∑ I : Grid X, ((I : Set X).indicator 1 x') *          ((D2_1_3 a * defaultA a ^ 5 * 2 ^ (3 / a : ℝ)) /          volume (ball (c I) (16 * D ^ s I)) *          ∑ J ∈ 𝓙' t u (c I) (s I), D ^ ((s J - s I) / (a : ℝ)) * ∫⁻ y in J, ‖f y‖ₑ) := by      congr! 2 with I      rw [← ENNReal.div_mul _ (.inr (by positivity)) (.inr (by finiteness)), mul_rotate (_ / _),        ← mul_div_assoc]      congr 2; ring    _ ≤ ∑ I : Grid X, ((I : Set X).indicator 1 x') *          (C7_1_6 a / volume (ball (c I) (16 * D ^ s I)) *          ∑ J ∈ 𝓙' t u (c I) (s I), D ^ ((s J - s I) / (a : ℝ)) * ∫⁻ y in J, ‖f y‖ₑ) := by      gcongr; exact le_C7_1_6 (four_le_a X)    _ = C7_1_6 a *        ∑ I : Grid X, ((I : Set X).indicator 1 x') *          (1 / volume (ball (c I) (16 * D ^ s I)) *          ∑ J ∈ 𝓙' t u (c I) (s I), D ^ ((s J - s I) / (a : ℝ)) * ∫⁻ y in J, ‖f y‖ₑ) := by      rw [Finset.mul_sum]; congr! 1 with I      simp_rw [← mul_assoc, ← mul_div_assoc, mul_one, mul_comm (C7_1_6 a : ℝ≥0∞)]    _ = _ := by      unfold boundaryOperator; congr! 2 with I      simp_rw [← indicator_mul_const, Pi.one_apply, one_mul]; congr! 2      rw [Finset.mul_sum]; congr! 2 with J hJ      rw [← mul_assoc, mul_comm (_ / _), ← mul_div_assoc, mul_one, ijIntegral]; congr! 1      exact lintegral_eq_lintegral_approxOnCube pairwiseDisjoint_𝓙 (mem_𝓙_of_mem_𝓙' hJ) hf