smaller_boundary

lemma smaller_boundary (n : ℕ) :    ∀ {k : ℤ}, (hk : -S ≤ k) → (hk_mnK : -S ≤ k - n * K') → ∀ (y : Yk X k),      ∑' (y' : Yk X (k - n * K')), ∑ᶠ (_ : clProp(hk_mnK,y'|hk,y)), volume (I3 hk_mnK y') ≤        2⁻¹ ^ n * volume (I3 hk y) := by  induction n with  | zero =>    intro k hk hk_mnK y    rw [boundary_sum_eq hk hk_mnK y]    simp only [Int.cast_ofNat_Int, pow_zero, one_mul]    gcongr    simp only [iUnion_subset_iff]    exact fun _ hy' => hy'.I3_subset  | succ n hinduction =>  intro k hk hk_mnK y  rw [boundary_sum_eq hk hk_mnK y]  calc    volume (⋃ (y'' : Yk X (k - (n + 1 : ℕ) * K')),      ⋃ (_:clProp(hk_mnK,y''|hk,y)), I3 hk_mnK y'')    ≤ volume (⋃ (y' : Yk X (k - K')), ⋃ (_ : clProp(le_s_2' n hk_mnK,y'|hk,y)),        ⋃ (y'' : Yk X (k - (n + 1 : ℕ) * K')),          ⋃ (_ : clProp(hk_mnK,y''|le_s_2' n hk_mnK,y')), I3 hk_mnK y'') := by      apply volume.mono      simp only [iUnion_subset_iff]      intro y'' hy'' x hx      push _ ∈ _      have hx_y: x ∈ I3 hk y := hy''.I3_subset hx      have : x ∈ ⋃ (y' : Yk X (k - K')), I3 (le_s_2' n hk_mnK) y' :=        cover_by_cubes (le_s_2' n hk_mnK) (by linarith) hk y hx_y      simp only [mem_iUnion] at this      obtain ⟨y', hx_y'⟩ := this      use y'      have hz : clProp(hk_mnK,y''|(le_s_2' n hk_mnK),y') ∧ clProp((le_s_2' n hk_mnK),y'|hk,y):= by        apply transitive_boundary hk_mnK (le_s_2' n hk_mnK) hk _ (by linarith) y'' y' y x _ hy''        · simp only [Nat.cast_add, Nat.cast_one]          rw [right_distrib, one_mul]          gcongr          trans 0 + ↑(@const_K a)          · rw [zero_add]          gcongr; positivity        · simp only [mem_inter_iff, and_assoc]          use hx      use hz.right, y'', hz.left    _ = ∑' (y' : Yk X (k - K')), ∑ᶠ (_ : clProp(le_s_2' n hk_mnK,y'|hk,y)),          volume (⋃ (y'' : Yk X (k - (n + 1 : ℕ) * K')),            ⋃ (_ : clProp(hk_mnK,y''|le_s_2' n hk_mnK,y')), I3 hk_mnK y'') := by      letI := (Yk_countable X (k - K')).to_subtype      rw [measure_iUnion]      · congr with y'        classical        by_cases h : clProp(le_s_2' n hk_mnK , y' | hk, y) <;> simp [h]      · intro i i' hneq        simp only [disjoint_iUnion_right, disjoint_iUnion_left]        intro _ y1 hy1i _ y2 hy2i'        apply Disjoint.mono_left hy2i'.I3_subset        apply Disjoint.mono_right hy1i.I3_subset        rw [Set.disjoint_iff]        intro x hx        exact hneq (I3_prop_1 _ hx)      intro y'      apply MeasurableSet.iUnion      intro _      letI := (Yk_countable X (k-(n+1:ℕ)*K')).to_subtype      apply MeasurableSet.iUnion      intro y''      apply MeasurableSet.iUnion (fun _ ↦ I3_measurableSet hk_mnK y'')    _ = ∑' (y' : Yk X (k - K')), ∑ᶠ (_ : clProp(le_s_2' n hk_mnK,y'|hk,y)),          ∑' (y'': Yk X (k - (n + 1 : ℕ) * K')), ∑ᶠ (_ : clProp(hk_mnK,y''|le_s_2' n hk_mnK,y')),            volume (I3 hk_mnK y'') := by      congr with y'      congr with hcly'      rw [boundary_sum_eq (le_s_2' n hk_mnK) hk_mnK y']    _ = ∑' (y' : Yk X (k - K')), ∑ᶠ (_ : clProp(le_s_2' n hk_mnK,y'|hk,y)),          ∑' (y'' : Yk X ((k - K') - n * K')), ∑ᶠ (_ : clProp(le_s_1' n hk_mnK,y''|le_s_2' n hk_mnK,y')),            volume (I3 (le_s_1' n hk_mnK) y'') := by      have : k - (n + 1 : ℕ) * K' = (k - K') - n * K' := by        rw [Nat.cast_add, Nat.cast_one,add_comm,right_distrib,one_mul,Int.sub_sub]      congr! 8    _ ≤ ∑' (y' : Yk X (k - K')), ∑ᶠ (_ : clProp(le_s_2' n hk_mnK,y'|hk,y)),          2⁻¹ ^ n * volume (I3 (le_s_2' n hk_mnK) y') := by      apply ENNReal.summable.tsum_le_tsum _ (ENNReal.summable)      intro y'      classical      by_cases h : clProp(le_s_2' n hk_mnK , y' | hk, y)      · rw [finsum_eq_if, finsum_eq_if]        simp_rw [if_pos h]        apply hinduction      · simp_all    _ = 2⁻¹ ^ n * ∑' (y' : Yk X (k - K')), ∑ᶠ (_ : clProp(le_s_2' n hk_mnK,y'|hk,y)),          volume (I3 (le_s_2' n hk_mnK) y') := by      rw [← ENNReal.tsum_mul_left]      congr with y'      classical      by_cases h : clProp(le_s_2' n hk_mnK , y' | hk, y) <;> simp [h]    _ ≤ 2⁻¹ ^ n * (2⁻¹ * volume (I3 hk y)) := by      gcongr      apply _root_.small_boundary    _ = 2⁻¹ ^ (n + 1) * volume (I3 hk y) := by      rw [pow_add, pow_one, mul_assoc]