TileStructure.Forest.square_function_count

lemma square_function_count (hJ : J ∈ 𝓙₆ t u₁) {s' : ℤ} :    ⨍⁻ x in J, (∑ I with s I = s J - s' ∧ Disjoint (I : Set X) (𝓘 u₁) ∧    ¬Disjoint (J : Set X) (ball (c I) (8 * D ^ s I)),    (ball (c I) (8 * D ^ s I)).indicator 1 x) ^ 2 ∂volume ≤ C7_6_4 a s' := by  rcases lt_or_ge (↑S + s J) s' with hs' | hs'  · suffices ({I : Grid X | s I = s J - s' ∧ Disjoint (I : Set X) (𝓘 u₁) ∧        ¬Disjoint (J : Set X) (ball (c I) (8 * D ^ s I)) } : Finset (Grid X)) = ∅ by      rw [this]      simp only [Finset.sum_empty, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, laverage_zero, zero_le]    simp only [Finset.filter_eq_empty_iff, Finset.mem_univ, not_and, Decidable.not_not,      true_implies]    intros I hI    have : -S ≤ s I := (range_s_subset ⟨I, rfl⟩).1    linarith  have : NeZero (volume.restrict (J : Set X) univ) := ⟨by    rw [Measure.restrict_apply_univ]    exact ((measure_ball_pos _ _ (by      simp only [defaultD, Nat.cast_pow, Nat.cast_ofNat, defaultA, Nat.ofNat_pos,        div_pos_iff_of_pos_right]; positivity)).trans_le      (measure_mono (μ := volume) (ball_subset_Grid (i := J)))).ne'⟩  have : IsFiniteMeasure (volume.restrict (J : Set X)) := ⟨by    rw [Measure.restrict_apply_univ]    exact volume_coeGrid_lt_top⟩  let 𝒟 (s₀ x) : Set (Grid X) := { I | x ∈ ball (c I) (8 * D ^ s I) ∧ s I = s₀ }  let supp : Set X := { x ∈ J | Metric.infEDist x Jᶜ ≤ 8 * (D ^ (s J - s')) }  have hsupp : supp ⊆ J := fun x hx ↦ hx.1  have vsupp : volume.real supp ≤ 2 * (↑8 * ↑D ^ (-s')) ^ κ * volume.real (J : Set X) := by    simp only [supp, sub_eq_neg_add, ENNReal.zpow_add (x := D) (by simp) (by finiteness),      ← mul_assoc]    convert! small_boundary (i := J) (t := 8 * ↑D ^ (-s')) ?_    · simp only [ENNReal.coe_mul, ENNReal.coe_ofNat]      rw [ENNReal.coe_zpow (by simp)]      norm_num    · rw [show (8 : ℝ≥0) = 2 ^ 3 by norm_num]      simp only [defaultD, Nat.cast_pow, Nat.cast_ofNat, defaultA, ← zpow_natCast, ← zpow_mul,        ← zpow_add₀ (show (2 : ℝ≥0) ≠ 0 by norm_num)]      gcongr      · norm_num      · simp only [Nat.cast_mul, Nat.cast_pow, mul_neg,        le_add_neg_iff_add_le, ← mul_add]        refine (Int.mul_nonpos_of_nonneg_of_nonpos (by positivity) ?_).trans (by norm_num)        rwa [← sub_nonpos, sub_eq_neg_add, neg_add] at hs'  have vsupp : volume supp ≤ ENNReal.ofReal (2 * (↑8 * ↑D ^ (-s')) ^ κ) * volume (J : Set X) := by    apply ENNReal.ofReal_le_ofReal at vsupp    rwa [Measure.real, Measure.real, ENNReal.ofReal_mul (by positivity),      ENNReal.ofReal_toReal (volume_coeGrid_lt_top.ne),      ENNReal.ofReal_toReal ((measure_mono hsupp).trans_lt volume_coeGrid_lt_top).ne] at vsupp  have est₁ (s₀ x) : (𝒟 s₀ x).toFinset.card ≤ (defaultA a) ^ 7 := by    apply Nat.cast_le (α := ℝ).mp    have : 0 < volume.real (ball x (9 * ↑D ^ s₀)) :=      ENNReal.toReal_pos (measure_ball_pos _ _ (by simpa using by positivity)).ne' (by finiteness)    refine le_of_mul_le_mul_right (a := volume.real (ball x (9 * D ^ s₀))) ?_ this    transitivity (defaultA a) ^ 7 * ∑ I ∈ 𝒟 s₀ x, volume.real (ball (c I) (D ^ s I / 4))    · rw [Finset.mul_sum, ← nsmul_eq_mul, ← Finset.sum_const]      refine Finset.sum_le_sum fun I hI ↦ ?_      simp only [mem_toFinset] at hI      apply le_trans _ (measureReal_ball_two_le_same_iterate (μ := volume) (c I) (D ^ s I / 4) 7)      refine measureReal_mono ?_ (by finiteness)      apply ball_subset_ball'      refine (add_le_add le_rfl hI.1.le).trans ?_      rw [div_eq_mul_one_div, mul_comm _ (1 / 4), hI.2, ← add_mul, ← mul_assoc]      gcongr      linarith    have disj : (𝒟 s₀ x).PairwiseDisjoint fun I : Grid X ↦ ball (c I) (D ^ s I / 4) := by      intros I₁ hI₁ I₂ hI₂ e      exact disjoint_of_subset ball_subset_Grid ball_subset_Grid        ((eq_or_disjoint (hI₁.2.trans hI₂.2.symm)).resolve_left e)    rw [← measureReal_biUnion_finset (by simpa only [coe_toFinset] using disj)      (fun _ _ ↦ measurableSet_ball) (by finiteness)]    simp only [Nat.cast_pow, Nat.cast_ofNat]    gcongr    · finiteness    · simp only [mem_toFinset, iUnion_subset_iff]      intro I hI      apply ball_subset_ball'      rw [dist_comm, div_eq_mul_one_div, mul_comm]      refine (add_le_add le_rfl hI.1.le).trans ?_      rw [← add_mul, hI.2]      gcongr      linarith  simp_rw [← Nat.cast_le (α := ℝ≥0∞)] at est₁  have est₂ (x) (hx : x ∈ J) : (∑ I with s I = s J - s' ∧ Disjoint (I : Set X) (𝓘 u₁) ∧      ¬Disjoint (J : Set X) (ball (c I) (8 * D ^ s I)),      (ball (c I) (8 * D ^ s I)).indicator (1 : X → ℝ≥0∞) x) ≤      if x ∈ supp then (defaultA a) ^ 7 else 0 := by    split_ifs with hx'    · rw [Finset.sum_indicator_eq_sum_filter]      simp only [Pi.one_apply, Finset.sum_const, nsmul_eq_mul, mul_one]      refine le_trans ?_ (est₁ (s J - s') x)      gcongr      intro I      simp_rw [Finset.filter_filter, Finset.mem_filter_univ, mem_toFinset]      exact fun H ↦ ⟨H.2, H.1.1⟩    · have (I : Grid X) : ball (c I) (8 * D ^ s I) = Metric.eball (c I) (8 * D ^ s I) := by        trans Metric.eball (c I) (show ℝ≥0 from ⟨8 * D ^ s I, by positivity⟩)        · rw [Metric.eball_coe]; rfl        · congr!          simp only [ENNReal.coe_nnreal_eq, ← Real.rpow_intCast]          erw [ENNReal.ofReal_mul (by norm_num)]          rw [← ENNReal.ofReal_rpow_of_pos (by simp), ENNReal.ofReal_natCast]          norm_num      simp_rw [this]      simp only [CharP.cast_eq_zero, nonpos_iff_eq_zero, Finset.sum_eq_zero_iff, Finset.mem_filter,        Finset.mem_univ, true_and, indicator_apply_eq_zero, Metric.mem_eball, Pi.one_apply,        one_ne_zero, imp_false, not_lt, and_imp]      intro I e hI₁ _      simp only [Grid.mem_def, mem_setOf_eq, not_and, not_le, supp, ← e] at hx'      exact (hx' hx).le.trans (iInf₂_le (c I)        fun h ↦ Set.disjoint_iff.mp hI₁ ⟨Grid.c_mem_Grid, hJ.2.1 h⟩)  have est₂' (x) (hx : x ∈ J) : _ ≤ supp.indicator (fun _ ↦ (↑(defaultA a ^ 7 : ℕ) : ℝ≥0∞) ^ 2) x :=    (pow_left_mono 2 <| est₂ x hx).trans (by simp [Set.indicator_apply])  refine (setLaverage_mono' coeGrid_measurable est₂').trans ?_  rw [laverage_eq, ENNReal.div_le_iff (NeZero.ne _) (by finiteness)]  refine (lintegral_indicator_const_le _ _).trans ?_  rw [Measure.restrict_apply' coeGrid_measurable, Measure.restrict_apply_univ,    Set.inter_eq_left.mpr (fun x hx ↦ hx.1)]  refine ((ENNReal.mul_le_mul_iff_right (by simp) (ne_of_beq_false rfl).symm).mpr vsupp).trans ?_  rw [← mul_assoc, ENNReal.ofReal, ← ENNReal.coe_natCast, ← ENNReal.coe_pow, ← ENNReal.coe_mul]  gcongr  rw [Real.toNNReal_mul (by positivity), Real.toNNReal_rpow_of_nonneg (by positivity),    Real.toNNReal_mul (by positivity), ← Real.rpow_intCast,    Real.toNNReal_rpow_of_nonneg (by positivity), Real.toNNReal_natCast]  simp only [Nat.cast_pow, Nat.cast_ofNat, Real.toNNReal_ofNat, Int.cast_neg, ← pow_mul]  rw [← mul_assoc, ← pow_succ, C7_6_4, ← NNReal.rpow_natCast, ← NNReal.rpow_intCast, Int.cast_neg]  congr!  simp [mul_assoc, mul_comm (G := ℝ) 14]