small_boundary'

lemma small_boundary' (k : ℤ) (hk : -S ≤ k) (hk_mK : -S ≤ k - K') (y : Yk X k) :    ∑' (z : Yk X (k - K')), volume (⋃ (_ : clProp(hk_mK,z|hk,y)), (I3 hk_mK z))      ≤ 2⁻¹ * volume (I3 hk y) := by  suffices    (K') * ∑' (z : Yk X (k - K')), volume (⋃ (_:clProp(hk_mK,z|hk,y)),I3 hk_mK z)      ≤ C4_1_7 X * volume (I3 hk y) by    rw [C4_1_7_eq X] at this    dsimp only [const_K] at this    nth_rw 1 [pow_add 2 (4 * a) 1] at this    rw [pow_one 2, Nat.cast_mul, Nat.cast_two, mul_comm _ 2, mul_assoc,      ENNReal.mul_le_iff_le_inv (by norm_num) (by norm_num), ← mul_assoc,mul_comm 2⁻¹ _,      mul_assoc] at this    simp only [Nat.cast_pow, Nat.cast_ofNat, ENNReal.coe_pow, ENNReal.coe_ofNat] at this    rw [← ENNReal.mul_le_mul_iff_right]    · exact this    · exact (NeZero.ne (2 ^ (4 * a)))    · finiteness  letI : Countable (Yk X (k - K')) := (Yk_countable X (k - K')).to_subtype  classical  calc    K' * ∑' (z : ↑(Yk X (k - K'))), volume (⋃ (_ : clProp(hk_mK,z|hk,y)), I3 hk_mK z)      = ∑ (_ : Ioc (k - K') k),        ∑'(z : Yk X (k - K')),volume (⋃ (_ : clProp(hk_mK,z|hk,y)), I3 hk_mK z) := by        rw [Finset.sum_const]        simp only [Finset.card_univ, Fintype.card_ofFinset, Int.card_Ioc, sub_sub_cancel,          Int.toNat_natCast, nsmul_eq_mul]    _ = ∑ (_ : Ioc (k - K') k), volume (        ⋃ (z : Yk X (k - K')),⋃ (_ : clProp(hk_mK,z|hk,y)),I3 hk_mK z) := by      apply Finset.sum_congr (rfl)      intro x      simp only [Finset.mem_univ, true_implies]      symm      classical      refine measure_iUnion ?_ ?_      · intro i i' hneq        simp only [disjoint_iUnion_right, disjoint_iUnion_left]        intro _ _        rw [Set.disjoint_iff]        intro x hx        apply hneq        exact I3_prop_1 hk_mK hx      · intro i        rw [Set.iUnion_eq_if]        by_cases h : (clProp(hk_mK, i | hk, y))        · rw [if_pos h]          exact I3_measurableSet hk_mK i        · simp [if_neg h]    _ ≤ ∑ (k' : Ioc (k - K') k),          volume (⋃ (z ∈ {z' : Yk X k' | clProp((le_s hk_mK k'),z'|hk,y) }),            I3 (le_s hk_mK k') z) := by      apply Finset.sum_le_sum      simp only [Finset.mem_univ, mem_setOf_eq, true_implies]      intro k'      apply volume.mono      simp only [iUnion_subset_iff]      intro z hz x hx      have : x ∈ I3 hk y := hz.I3_subset hx      have : x ∈ ⋃ z, I3 (le_s hk_mK k') z:=        cover_by_cubes (le_s hk_mK k') (k'.property.right) hk y this      simp only [mem_iUnion] at this      obtain ⟨y', hy'⟩ := this      simp only [mem_iUnion, exists_prop]      use y'      constructor      · apply And.right        apply transitive_boundary hk_mK (le_s hk_mK k') hk k'.property.left.le k'.property.right z y' y        · simp only [mem_inter_iff]          exact And.intro (And.intro hx hy') this        · exact hz      exact hy'    _ = ∑ (k' : Ioc (k - K') k), ∑' (z : Yk X k'),          volume (⋃ (_ : clProp((le_s hk_mK k'),z|hk,y)), I3 (le_s hk_mK k') z) := by      apply Finset.sum_congr (rfl)      intro k'      simp only [Finset.mem_univ, true_implies]      letI := (Yk_countable X k').to_subtype      refine measure_iUnion ?_ ?_      · intro i i' hneq        simp only [mem_setOf_eq, disjoint_iUnion_right, disjoint_iUnion_left]        intro _ _        rw [Set.disjoint_iff]        intro x hx        exact hneq <| I3_prop_1 _ hx      intro i      apply MeasurableSet.iUnion      intro _      exact I3_measurableSet (le_s hk_mK k') i    _ ≤ ∑ (k' : Ioc (k - K') k), ∑' (z : Yk X k'), C4_1_7 X *          volume (⋃ (_ : clProp((le_s hk_mK k'),z|hk,y)), ball (z : X) (4⁻¹ * D ^ (k' : ℤ))) := by      apply Finset.sum_le_sum      intro k'      simp only [Finset.mem_univ, true_implies]      apply ENNReal.summable.tsum_le_tsum _ (ENNReal.summable)      intro z      simp_rw [iUnion_eq_if,apply_ite volume,measure_empty, mul_ite, mul_zero]      by_cases h : clProp(le_s hk_mK k',z|hk,y)      · simp_rw [if_pos h]        exact volume_tile_le_volume_ball (↑k') (le_s hk_mK k') z      · repeat rw [if_neg h]    _ = C4_1_7 X * ∑ (k' : Ioc (k - K') k), ∑' (z : Yk X k'),          volume (⋃ (_ : clProp((le_s hk_mK k'),z|hk,y)), ball (z : X) (4⁻¹ * D ^ (k' : ℤ))) := by      rw [Finset.mul_sum]      apply Finset.sum_congr (rfl)      simp only [Finset.mem_univ, true_implies]      intro k'      rw [ENNReal.tsum_mul_left]    _ = C4_1_7 X * ∑ (k' : Ioc (k - K') k),          volume (⋃ (z : Yk X k'), ⋃ (_ : clProp((le_s hk_mK k'),z|hk,y)),            ball (z : X) (4⁻¹ * D ^ (k' : ℤ))) := by      congr      ext k'      symm      letI := (Yk_countable X k').to_subtype      apply measure_iUnion _ <| fun _ ↦ MeasurableSet.iUnion <| fun _ ↦ measurableSet_ball      intro i i' hneq      simp only [disjoint_iUnion_right, disjoint_iUnion_left]      intro _ _      apply Disjoint.mono      · trans ball (i : X) (2⁻¹ * D ^ (k' : ℤ))        · apply ball_subset_ball          gcongr          linarith        apply I3_prop_3_1        have := k'.property.left        linarith      · trans ball (i' : X) (2⁻¹ * D ^ (k' : ℤ))        · apply ball_subset_ball          gcongr          norm_num        apply I3_prop_3_1        have := k'.property.left        linarith      rw [Set.disjoint_iff]      intro x hx      exact hneq <| I3_prop_1 _ hx    _ ≤ C4_1_7 X * ∑' (k' : Ioc (k - K') k),          volume (⋃ (z : Yk X k'), ⋃ (_:clProp((le_s hk_mK k'),z|hk,y)),            ball (z : X) (4⁻¹ * D ^ (k' : ℤ))) := by      gcongr      exact ENNReal.sum_le_tsum Finset.univ    _ = C4_1_7 X * volume (⋃ (k' : Ioc (k - K') k), ⋃ (z:Yk X k'),          ⋃ (_ : clProp((le_s hk_mK k'),z|hk,y)), ball (z : X) (4⁻¹ * D ^ (k' : ℤ))) := by      congr      symm      apply measure_iUnion      · rw [Std.Symm.pairwise_on]        · intro l' l hl          simp only [disjoint_iUnion_right, disjoint_iUnion_left]          intro u hu u' hu'          rw [Set.disjoint_iff]          obtain ⟨x, hx⟩ := Metric.infEDist_lt_iff.mp hu'.I3_infdist_lt          intro x' hx'          have : x ∈ ball (u:X) (2⁻¹ * D^(l:ℤ)) := by            simp only [mem_inter_iff, mem_compl_iff, mem_ball] at hx hx' ⊢            calc              dist x (u:X)                ≤ dist x (u':X) + dist (u':X) x' + dist x' (u:X) := dist_triangle4 x (↑u') x' ↑u              _ < 6 * D^(l':ℤ ) + 4⁻¹ * D^(l':ℤ) + 4⁻¹ * D^(l:ℤ) := by                rw [← dist_comm x' u']                apply add_lt_add _ hx'.right                apply add_lt_add _ hx'.left                rw [dist_edist]                rw [← @ENNReal.toReal_ofReal (6 * D ^ (l':ℤ)), ← Real.rpow_intCast]                · rw [ENNReal.toReal_lt_toReal (by finiteness) (by finiteness),                    ENNReal.ofReal_mul (by norm_num), ENNReal.ofReal_ofNat,                    ← ENNReal.ofReal_rpow_of_pos (realD_pos a), ENNReal.ofReal_natCast,                    edist_comm, ENNReal.rpow_intCast]                  exact hx.right                positivity              _ = 4⁻¹ * 25 * D^(l':ℤ) + 4⁻¹ * D^(l:ℤ) := by                rw [← right_distrib]                norm_num              _ ≤ 4⁻¹ * D^(l:ℤ) + 4⁻¹ * D^(l:ℤ) := by                rw [add_le_add_iff_right, mul_assoc]                gcongr                trans D * D^(l':ℤ)                · gcongr                  exact twentyfive_le_realD X                nth_rw 1 [← zpow_one (D:ℝ)]                rw [← zpow_add₀ (realD_pos a).ne.symm]                have : (l':ℤ) < l := hl                exact zpow_le_zpow_right₀ (one_le_realD a) (by linarith)              _ = 2⁻¹ * D^(l:ℤ) := by                rw [← two_mul _,← mul_assoc]                norm_num          have : x ∈ I3 hk y := by            apply dyadic_property (le_s hk_mK l) (l.property.right) hk            · rw [Set.not_disjoint_iff]              use x, I3_prop_3_1 (le_s hk_mK l) u this              apply hu.I3_subset              exact I3_prop_3_1 (le_s hk_mK l) u this            exact I3_prop_3_1 (le_s hk_mK l) u this          exact hx.left this      intro k'      letI := (Yk_countable X k').to_subtype      apply MeasurableSet.iUnion <| fun _ ↦ MeasurableSet.iUnion <| fun _ ↦ measurableSet_ball    _ ≤ C4_1_7 X * volume (I3 hk y) := by      gcongr      simp only [iUnion_subset_iff]      intro k' y' hy' x      apply Subset.trans _ hy'.I3_subset      apply Subset.trans _ (I3_prop_3_1 _ _)      apply ball_subset_ball      gcongr      norm_num