TileStructure.Forest.gtc_integral_bound

lemma gtc_integral_bound {k : ℤ} {ℭ : Set (𝔓 X)}    (hs : ∀ p ∈ ℭ, ¬Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (16 * D ^ s J)) → s J ≤ 𝔰 p) :    ∑ p ∈ ℭ with ¬Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (16 * D ^ s J)) ∧ 𝔰 p = k,      ∫⁻ x in E p, ‖f x‖ₑ ≤    ∫⁻ x in ball (c J) (32 * D ^ k), ‖f x‖ₑ := by  set V := ℭ.toFinset.filter      (fun p ↦ ¬Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (16 * D ^ s J)) ∧ 𝔰 p = k)  calc    _ = ∫⁻ x in ⋃ p ∈ V, E p, ‖f x‖ₑ := by      refine (lintegral_biUnion_finset (fun p₁ mp₁ p₂ mp₂ hn ↦ ?_)        (fun _ _ ↦ measurableSet_E) _).symm      contrapose! hn; obtain ⟨x, mx₁ : x ∈ E p₁, mx₂ : x ∈ E p₂⟩ := not_disjoint_iff.mp hn      rw [E, mem_setOf] at mx₁ mx₂      simp_rw [Finset.mem_coe, V, Finset.mem_filter, mem_toFinset] at mp₁ mp₂      have i_eq := mp₂.2.2 ▸ mp₁.2.2      replace i_eq : 𝓘 p₁ = 𝓘 p₂ :=        (eq_or_disjoint i_eq).resolve_right (not_disjoint_iff.mpr ⟨x, mx₁.1, mx₂.1⟩)      by_contra! h      exact absurd (disjoint_Ω h i_eq) (not_disjoint_iff.mpr ⟨Q x, mx₁.2.1, mx₂.2.1⟩)    _ ≤ _ := by      refine lintegral_mono_set (iUnion₂_subset fun p mp ↦ ?_)      simp_rw [V, Finset.mem_filter, mem_toFinset] at mp; specialize hs p mp.1 mp.2.1      refine (E_subset_𝓘.trans Grid_subset_ball).trans (ball_subset_ball' ?_)      rw [← mp.2.2]; change (4 : ℝ) * D ^ 𝔰 p + dist (𝔠 p) (c J) ≤ _      calc        _ ≤ (4 : ℝ) * D ^ 𝔰 p + 8 * D ^ 𝔰 p + 16 * D ^ s J := by          rw [add_assoc]; gcongr; exact (dist_lt_of_not_disjoint_ball mp.2.1).le        _ ≤ (4 : ℝ) * D ^ 𝔰 p + 8 * D ^ 𝔰 p + 16 * D ^ 𝔰 p := by gcongr; exact one_le_realD a        _ ≤ _ := by rw [← add_mul, ← add_mul]; gcongr; norm_num