boundary_measure

lemma boundary_measure {k : ℤ} (hk : -S ≤ k) (y : Yk X k) {t : ℝ≥0} (ht : t ∈ Set.Ioo 0 1)    (htD : (D ^ (-S : ℤ) : ℝ) ≤ t * D ^ k) :    volume ({x | x ∈ I3 hk y ∧ Metric.infEDist x (I3 hk y)ᶜ ≤ (↑t * ↑D ^ k)}) ≤      2 * t ^ κ * volume (I3 hk y) := by  have hconst_n : -S ≤ k - const_n a ht * K' := by    suffices (D ^ (-S : ℤ) : ℝ) ≤ D ^ (k - const_n a ht * K' : ℤ) by      simp_rw [← Real.rpow_intCast] at this      rw [Real.rpow_le_rpow_left_iff (one_lt_realD X)] at this      simp only [Int.cast_le] at this      exact this    exact htD.trans (const_n_prop_2 X ht k)  have hconst_n_k : k - const_n a ht * K' ≤ k := by    simp only [tsub_le_iff_right, le_add_iff_nonneg_right]    positivity  simp only [mem_Ioo] at ht  calc    volume ({x | x ∈ I3 hk y ∧ Metric.infEDist x (I3 hk y)ᶜ ≤ (↑t * ↑D ^ k)})    _ ≤ volume (⋃ (y' : Yk X (k - const_n a ht *K')), ⋃ (_ : clProp(hconst_n,y'|hk,y)),          I3 hconst_n y') := by      apply volume.mono      intro x      simp only [mem_setOf_eq, NNReal.val_eq_coe, and_imp]      intro hxi3 hxb'      have : x ∈ ⋃ (y' : Yk X (k - const_n a ht * K')), I3 hconst_n y' :=        cover_by_cubes hconst_n hconst_n_k hk y hxi3      simp only [mem_iUnion] at this ⊢      obtain ⟨y', hy'⟩ := this      have hxy' : x ∈ ball (y' : X) (4 * D ^ (k - const_n a ht * K')) := by        apply I3_prop_3_2        exact hy'      refine ⟨y', ⟨?_, ?_⟩, hy'⟩      · apply dyadic_property hconst_n hconst_n_k hk y y'        rw [not_disjoint_iff]        use x      rw [← eball_ofReal, Metric.mem_eball, ENNReal.ofReal_mul (by norm_num), ENNReal.ofReal_ofNat,        ← Real.rpow_intCast, ← ENNReal.ofReal_rpow_of_pos (realD_pos a),        ENNReal.ofReal_natCast,ENNReal.rpow_intCast,edist_comm] at hxy'      have : 0 < (Nat.cast D : ℝ≥0∞) := by        rw [← ENNReal.ofReal_natCast,ENNReal.ofReal_pos]        exact realD_pos a      calc        Metric.infEDist (y' : X) (I3 hk y)ᶜ        _ ≤ Metric.infEDist (x:X) (I3 hk y)ᶜ + edist (y':X) x :=          Metric.infEDist_le_infEDist_add_edist        _ < t * D^k + 4 * D^(k-const_n a ht * K') := by          apply ENNReal.add_lt_add_of_le_of_lt _ hxb' hxy'          apply (hxb'.trans_lt _).ne          finiteness        _ ≤ D ^ (k - const_n a ht * K') + 4 * D ^ (k - const_n a ht * K') := by          rw [ENNReal.add_le_add_iff_right]          · have := const_n_prop_2 X ht k            nth_rw 1 [NNReal.val_eq_coe] at this            simp_rw [← Real.rpow_intCast] at this            rw [← ENNReal.ofReal_le_ofReal_iff (by positivity),              ENNReal.ofReal_mul (by exact ht.left.le), ENNReal.ofReal_coe_nnreal,              ← ENNReal.ofReal_rpow_of_pos (realD_pos a),              ← ENNReal.ofReal_rpow_of_pos (realD_pos a), ENNReal.ofReal_natCast,              ENNReal.rpow_intCast, ENNReal.rpow_intCast] at this            exact this          finiteness        _ ≤ 6 * ↑D ^ (k - const_n a ht * ↑const_K) := by          nth_rw 1 [← one_mul (D ^ (k - const_n a ht * K') : ℝ≥0∞), ← right_distrib]          rw [ENNReal.mul_le_mul_iff_left]          · norm_num          · apply LT.lt.ne'            rw [← ENNReal.rpow_intCast]            exact ENNReal.rpow_pos this (by finiteness)          finiteness    _ = ∑' (y' : Yk X (k - const_n a ht * K')), ∑ᶠ(_ : clProp(hconst_n, y'|hk, y)),          volume (I3 hconst_n y') := by rw [boundary_sum_eq hk hconst_n y]    _ ≤ 2⁻¹ ^ (const_n a ht) * volume (I3 hk y) := by apply smaller_boundary    _ ≤ 2 * t ^ κ * volume (I3 hk y) := by      refine mul_le_mul' ?_ (le_refl _)      suffices hsuf : ((2⁻¹ ^ (const_n a ht) : ℝ≥0) : ℝ≥0∞) ≤ (2 * t ^ κ : ℝ≥0) by        push_cast at hsuf        rw [ENNReal.coe_rpow_def]        have : ¬(t = 0 ∧ κ < 0) := by          push Not          intro h          by_contra          exact ht.left.ne h.symm        rw [if_neg this]        exact hsuf      rw [ENNReal.coe_le_coe]      calc        (2⁻¹ ^ const_n a ht : ℝ)        _ = 2 ^ (-const_n a ht : ℝ) := by          rw [Real.rpow_neg (by norm_num), ← Real.rpow_natCast,Real.inv_rpow (by norm_num)]        _ = (D ^ ((Real.logb 2 D)⁻¹)) ^ (-const_n a ht : ℝ) := by          rw [Real.inv_logb, Real.rpow_logb (realD_pos a) (one_lt_realD X).ne' (by norm_num)]        _ = D ^ ((const_n a ht * K' : ℝ) * -(Real.logb 2 D * K' : ℝ)⁻¹) := by          rw [← Real.rpow_mul <| realD_nonneg a]          congr 1          rw [mul_neg, mul_neg]          congr 1          rw [mul_inv, mul_assoc, mul_comm (K' : ℝ), mul_assoc, inv_mul_cancel₀ K_pos.ne',            mul_one, mul_comm]        _ = (D ^ (const_n a ht * K' : ℝ) : ℝ)⁻¹ ^ (Real.logb 2 D * K' : ℝ)⁻¹ := by          rw [Real.rpow_mul (realD_nonneg a), Real.rpow_neg (by positivity),            Real.inv_rpow (by positivity)]        _ ≤ (t * D ^(K' : ℝ)) ^ (Real.logb 2 D * K' : ℝ)⁻¹ := by          rw [Real.rpow_le_rpow_iff]          · rw [inv_le_comm₀]            · rw [← Nat.cast_mul, Real.rpow_natCast, Real.rpow_natCast]              exact const_n_prop_3 X ht            · exact Real.rpow_pos_of_pos (realD_pos a) _            · rw [mul_pos_iff_of_pos_right]              · exact ht.left              · exact Real.rpow_pos_of_pos (realD_pos a) _          · positivity          · positivity          · rw [inv_pos, mul_pos_iff_of_pos_right (K_pos)]            exact Real.logb_pos (by norm_num) (one_lt_realD X)        _ = 2 * t ^ (Real.logb 2 D * K' : ℝ)⁻¹ := by          rw [Real.mul_rpow,mul_comm, ← Real.rpow_mul (realD_nonneg a), mul_comm (K' : ℝ)]          · rw [mul_inv, mul_assoc, inv_mul_cancel₀ K_pos.ne', mul_one, Real.inv_logb,              Real.rpow_logb (realD_pos a) (one_lt_realD X).ne' (by norm_num)]          · exact ht.left.le          positivity        _ ≤ (2 * t ^ κ : ℝ) := by          rw [mul_le_mul_iff_right₀ (by linarith)]          have : (t : ℝ) ∈ Ioo 0 1 := ht          rw [mem_Ioo] at this          rw [Real.rpow_le_rpow_left_iff_of_base_lt_one (this.left) (this.right)]          exact kappa_le_log2D_inv_mul_K_inv X