TileStructure.Forest.local_dens2_tree_bound

lemma local_dens2_tree_bound (hu : u ∈ t) (hJ : J ∈ 𝓙 (t u)) :    volume (F ∩ J) ≤ C7_3_3 a * dens₂ (t u) * volume (J : Set X) := by  by_cases J_top : J = topCube  · have ⟨p, hpu⟩ := t.nonempty hu    have S0 : S = 0 := S_eq_zero_of_topCube_mem_𝓙₀ (t.nonempty hu) (𝓙_subset_𝓙₀ (J_top ▸ hJ))    have 𝓘p_eq_J : 𝓘 p = J := ((𝓘 p).eq_topCube_of_S_eq_zero S0).trans J_top.symm    apply local_dens2_tree_bound_aux' hpu (𝓘p_eq_J ▸ Grid_subset_ball)    exact 𝓘p_eq_J ▸ le_mul_of_one_le_left zero_le (one_le_pow_of_one_le' one_le_two _)  have ⟨J', hJJ', hsJ'⟩ := J.exists_scale_succ (J.scale_lt_scale_topCube J_top)  have : J' ∉ 𝓙₀ (t u) := fun h ↦ succ_ne_self (s J) <| hJ.eq_of_le h hJJ' ▸ hsJ'.symm  rw [𝓙₀, mem_setOf_eq] at this  push Not at this  obtain ⟨p, hpu, hp⟩ := this.2  have d0 := realD_pos a  have volume_le : volume (ball (c J') (204 * D ^ (s J' + 1))) ≤                     2 ^ (2 * 𝕔 * a ^ 3 + 10 * a) * volume (J : Set X) := calc    _ ≤ volume (ball (c J) ((204 * D + 4) * D ^ (s J'))) := by      refine measure_mono <| ball_subset_ball' ?_      rw [add_mul, mul_assoc, zpow_add₀ d0.ne.symm, mul_comm (D : ℝ), zpow_one]      apply add_le_add_right (mem_ball'.mp <| Grid_subset_ball <| hJJ'.1 J.c_mem_Grid).le    _ ≤ volume (ball (c J) (2 ^ (2 * 𝕔 * a ^ 2 + 8) * D ^ (s J))) := by      rw [hsJ', zpow_add₀ d0.ne.symm, mul_comm ((D : ℝ) ^ (s J)), ← mul_assoc, zpow_one]      refine measure_mono (ball_subset_ball <| mul_le_mul_of_nonneg_right ?_ (zpow_pos d0 (s J)).le)      calc          _ ≤ 2 ^ 8 * (D : ℝ) ^ 2   := by nlinarith [one_lt_realD X]          _ = 2 ^ (2 * 𝕔 * a ^ 2 + 8) := by norm_cast; rw [pow_add, defaultD, ← pow_mul]; ring_nf    _ ≤ (defaultA a) ^ (2 * 𝕔 * a ^ 2 + 10) * volume (ball (c J) (D ^ (s J) / 4)) := by        rw [show 2 ^ (2 * 𝕔 * a^2 + 8) * (D : ℝ) ^ s J = 2 ^ (2 * 𝕔 * a^2 + 10) * (D ^ s J / 4) by ring]        apply measure_ball_two_le_same_iterate    _ ≤ 2 ^ (2 * 𝕔 * a ^ 3 + 10 * a) * volume (J : Set X) := by      apply le_of_le_of_eq <| mul_le_mul_right (measure_mono ball_subset_Grid) _      simp_rw [defaultA, Nat.cast_pow, Nat.cast_ofNat]      rw [← pow_mul, mul_comm a, add_mul, mul_assoc, show a ^ 2 * a = a ^ 3 by rfl]  by_cases hJB : (J : Set X) ⊆ ball (𝔠 p) (4 * D ^ (𝔰 p))  · refine local_dens2_tree_bound_aux' hpu hJB <| (measure_mono ?_).trans volume_le    exact hp.trans <| by gcongr; norm_num  have hcJ' : dist (c J') (𝔠 p) < 100 * (D : ℝ) ^ (s J' + 1) := by    refine mem_ball'.mp <| hp <| ball_subset_Grid <| mem_ball.mpr ?_    rw [𝔠, c, dist_self]    positivity  have hJp : (J : Set X) ⊆ ball (𝔠 p) (104 * D ^ (s J' + 1)) := by    rw [show (104 : ℝ) = 4 + 100 by norm_num, add_mul]    refine (hJJ'.1.trans Grid_subset_ball).trans <| ball_subset_ball' ?_    gcongr    exacts [one_le_realD _, Int.le.intro 1 rfl, hcJ'.le]  apply local_dens2_tree_bound_aux hpu (le_of_not_ge (hJB <| hJp.trans <| ball_subset_ball ·)) hJp  have B_subset : ball (𝔠 p) (104 * D ^ (s J' + 1)) ⊆ ball (c J') (204 * D ^ (s J' + 1)) := by    apply ball_subset_ball'    rw [show (204 : ℝ) = 104 + 100 by norm_num, add_mul]    exact add_le_add_right (dist_comm (c J') (𝔠 p) ▸ hcJ'.le) (104 * (D : ℝ) ^ (s J' + 1))  refine (measure_mono B_subset).trans <| volume_le.trans <| mul_le_mul_left ?_ _  rw [C7_3_3]  norm_cast  exact pow_le_pow_right' one_le_two (le_C7_3_3_exponent (four_le_a X) 10 (by norm_num))