TileStructure.Forest.local_dens1_tree_bound

lemma local_dens1_tree_bound (hu : u ∈ t) (hL : L ∈ 𝓛 (t u)) :    volume (L ∩ G ∩ ⋃ p ∈ t u, E p) ≤ C7_3_2 a * dens₁ (t u) * volume (L : Set X) := by  by_cases hq : (L : Set X) ∩ ⋃ p ∈ t u, E p = ∅  · rw [inter_comm (L : Set X), inter_assoc, hq, inter_empty, measure_empty]; exact zero_le  rw [← disjoint_iff_inter_eq_empty, disjoint_iUnion₂_right] at hq; push Not at hq  by_cases! hp₂ : ∃ p ∈ t u, ¬Disjoint (L : Set X) (E p) ∧ 𝔰 p ≤ s L  · exact local_dens1_tree_bound_exists hu hL hp₂  obtain ⟨p, mp, hp⟩ := hq; have sLp := hp₂ p mp hp  have lip : L < 𝓘 p := by    refine Grid.lt_def.mpr ⟨(le_of_mem_𝓛 hL mp ?_).1, sLp⟩    contrapose! hp; exact (hp.mono_left E_subset_𝓘).symm  obtain ⟨L', lL', sL'⟩ := Grid.exists_scale_succ sLp  replace lL' : L < L' := Grid.lt_def.mpr ⟨lL'.1, by lia⟩  obtain ⟨p'', mp'', lp''⟩ : ∃ p'' ∈ t u, 𝓘 p'' ≤ L' := by    have L'nm : L' ∉ 𝓛₀ (t u) := by      by_contra h      simp_rw [𝓛, mem_setOf, maximal_iff] at hL      exact lL'.ne (hL.2 h lL'.le)    rw [𝓛₀, mem_setOf, not_or, not_and_or] at L'nm; push Not at L'nm    have nfa : ¬∀ p ∈ t u, ¬L' ≤ 𝓘 p := by      push Not; refine ⟨p, mp, Grid.le_dyadic ?_ lL'.le lip.le⟩; change s L' ≤ 𝔰 p; lia    simp_rw [nfa, false_or] at L'nm; exact L'nm.2  suffices ∃ p' ∈ lowerCubes (t u),      𝓘 p' = L' ∧ dist_(p') (𝒬 p') (𝒬 u) < 4 ∧ smul 9 p'' ≤ smul 9 p' by    obtain ⟨p', mp', ip', dp', sp'⟩ := this    calc      _ ≤ volume (E₂ 9 p') := by        refine measure_mono fun x ⟨⟨mxL, mxG⟩, mxU⟩ ↦ ?_        have mxp' : x ∈ L' := lL'.le.1 mxL        rw [← ip'] at mxp'; refine ⟨⟨mxp', mxG⟩, ?_⟩        rw [mem_iUnion₂] at mxU; obtain ⟨q, mq, hq⟩ := mxU; rw [smul_snd, mem_preimage]        have p'lq : 𝓘 p' ≤ 𝓘 q := by          refine le_of_mem_of_mem ?_ mxp' (E_subset_𝓘 hq)          change s (𝓘 p') ≤ 𝔰 q; rw [ip']; suffices s L < 𝔰 q by lia          exact hp₂ q mq (not_disjoint_iff.mpr ⟨x, mxL, hq⟩)        apply (@mem_ball' ..).mpr        calc          _ ≤ dist_(p') (𝒬 p') (𝒬 u) + dist_(p') (𝒬 u) (𝒬 q) + dist_(p') (𝒬 q) (Q x) :=            dist_triangle4 ..          _ ≤ dist_(p') (𝒬 p') (𝒬 u) + dist_(q) (𝒬 u) (𝒬 q) + dist_(q) (𝒬 q) (Q x) := by            gcongr <;> exact Grid.dist_mono p'lq          _ < 4 + 4 + 1 := by            gcongr            · exact t.dist_lt_four' hu mq            · rw [← mem_ball']; exact subset_cball hq.2.1          _ = _ := by norm_num      _ ≤ 9 ^ a * dens₁ (t u) * volume (L' : Set X) := by        rw [← ip']        exact volume_E₂_le_dens₁_mul_volume mp' mp'' (by norm_num) sp'      _ ≤ 2 ^ (4 * a) * 2 ^ (𝕔 * a ^ 3 + 5 * a) * dens₁ (t u) * volume (L : Set X) := by        rw [show 2 ^ (4 * a) * _ * dens₁ (t u) * volume (L : Set X) =          2 ^ (4 * a) * dens₁ (t u) * (2 ^ (𝕔 * a ^ 3 + 5 * a) * volume (L : Set X)) by ring]        gcongr ?_ * _ * ?_        · norm_cast; rw [pow_mul]; exact pow_le_pow_left' (by norm_num) a        · exact volume_bound_of_Grid_lt lL'.le sL'      _ ≤ _ := by        gcongr; rw [C7_3_2]; norm_cast; rw [← pow_add]; apply Nat.pow_le_pow_right zero_lt_two        rw [← add_assoc, ← add_rotate, ← add_mul, show 4 + 5 = 9 by norm_num]        calc          _ ≤ 4 * 4 * a + 𝕔 * a ^ 3 := by gcongr; norm_num          _ ≤ a * a * a + 𝕔 * a ^ 3 := by gcongr <;> exact four_le_a X          _ = _ := by ring  obtain lp'' | lp'' := lp''.eq_or_lt  · use p'', subset_lowerCubes mp'', lp'', t.dist_lt_four hu mp''  have m₁ := biUnion_Ω (i := L') (range_𝒬 (mem_range_self u))  rw [mem_iUnion₂] at m₁; obtain ⟨p', mp', hp'⟩ := m₁  rw [mem_preimage, mem_singleton_iff] at mp'; change 𝓘 p' = L' at mp'  have ip'lp : 𝓘 p' ≤ 𝓘 p := by    rw [mp']; refine Grid.le_dyadic ?_ lL'.le lip.le; change s L' ≤ 𝔰 p; lia  use p', mem_lowerCubes.mp ⟨p, mp, ip'lp⟩, mp'; constructor  · rw [← mem_ball']; exact mem_of_mem_of_subset (subset_cball hp') (ball_subset_ball (by norm_num))  · rw [← mp'] at lp''    refine ⟨lp''.le, fun x mx ↦ ?_⟩    calc      _ ≤ dist_(p'') x (𝒬 p') + dist_(p'') (𝒬 p') (𝒬 u) + dist_(p'') (𝒬 u) (𝒬 p'') :=        dist_triangle4 ..      _ ≤ C2_1_2 a * (dist_(p') x (𝒬 p') + dist_(p') (𝒬 p') (𝒬 u)) + dist_(p'') (𝒬 u) (𝒬 p'') := by        rw [mul_add]; gcongr <;> exact Grid.dist_strictMono lp''      _ < C2_1_2 a * (9 + 1) + 4 := by        gcongr        · unfold C2_1_2; positivity        · exact mx        · rw [← mem_ball']; exact subset_cball hp'        · exact t.dist_lt_four' hu mp''      _ ≤ 1 / 256 * 10 + 4 := by        rw [show (9 : ℝ) + 1 = 10 by norm_num]; gcongr; exact C2_1_2_le_inv_256 X      _ < _ := by norm_num