TileStructure.Forest.limited_scale_impact_second_estimate

lemma limited_scale_impact_second_estimate (hp : p ∈ t u₂ \ 𝔖₀ t u₁ u₂) (hJ : J ∈ 𝓙₅ t u₁ u₂)    (h : ¬Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (8⁻¹ * D ^ s J))) :    𝔰 p ≤ s J + 3 := by  by_contra! three  have ⟨J', belongs, plusOne⟩ : ∃ J', J ≤ J' ∧ s J' = s J + 1 :=    Grid.exists_scale_succ (by change s J < 𝔰 p; linarith)  have ⟨p', ⟨_, distance⟩, hundred⟩ :      ∃ p' ∈ t.𝔖₀ u₁ u₂, ↑(𝓘 p') ⊆ ball (c J') (100 * D ^ (s J + 2)) := by    rw [← one_add_one_eq_two, ← add_assoc, ← plusOne]    have J'Touches𝔖₀ : J' ∉ 𝓙₀ (t.𝔖₀ u₁ u₂) := bigger_than_𝓙_is_not_in_𝓙₀ (le := belongs)      (sle := by linarith [plusOne]) (A_in := hJ.1)    rw [𝓙₀, Set.notMem_setOf_iff] at J'Touches𝔖₀    push Not at J'Touches𝔖₀    exact J'Touches𝔖₀.right  apply calculation_9 (X := X)  apply one_le_of_le_mul_right₀ (b := 2 ^ ((Z : ℝ) * n / 2)) (by positivity)  have DIsPos := realD_pos a  calc 2 ^ ((Z : ℝ) * (n : ℝ) / 2)    _ ≤ dist_{𝓘 p'} (𝒬 u₁) (𝒬 u₂) := by      exact distance    _ ≤ dist_{c J', 100 * D ^ (s J + 2)} (𝒬 u₁) (𝒬 u₂) := by      apply cdist_mono      intros x hx      exact hundred (ball_subset_Grid hx)    _ ≤ 2 ^ ((-𝕔 : ℝ) * a) * dist_{c J', 100 * D^(s J + 3)} (𝒬 u₁) (𝒬 u₂) := by      apply calculation_8      rw [mul_comm, calculation_6 a (s J), calculation_7 a (s J)]      exact_mod_cast le_cdist_iterate (k := 𝕔 * a) (f := 𝒬 u₁) (g := 𝒬 u₂) (hr := by positivity)    _ ≤ 2 ^ ((-𝕔 : ℝ) * a) * dist_{𝔠 p, 10 * D^(𝔰 p)} (𝒬 u₁) (𝒬 u₂) := by      gcongr      apply cdist_mono      simp only [not_disjoint_iff] at h      rcases h with ⟨middleX, lt_2, lt_3⟩      have lt_4 := Grid.dist_c_le_of_subset belongs.left      intros x lt_1      calc dist x (𝔠 p)      _ ≤ dist x (c J') + dist (c J') (c J) + dist (c J) middleX + dist middleX (𝔠 p) := by        exact dist_triangle5 x (c J') (c J) middleX (𝔠 p)      _ < 10 * D ^ 𝔰 p := by        simp only [mem_ball] at lt_3        rw [dist_comm] at lt_3 lt_4        exact calculation_4 (lt_1 := lt_1) (lt_2 := lt_2) (lt_3 := lt_3) (lt_4 := lt_4)          (three := three) (plusOne := plusOne) (X := X)    _ ≤ 2 ^ ((-(𝕔 - 6) : ℝ) * a) * dist_{𝓘 p} (𝒬 u₁) (𝒬 u₂) := by      apply calculation_5      have bigger : 0 < (D : ℝ) ^ 𝔰 p / 4 := by positivity      calc dist_{𝔠 p, 10 * D^(𝔰 p)} (𝒬 u₁) (𝒬 u₂)      _ ≤ dist_{𝔠 p, 2 ^ 6 * (D ^ 𝔰 p / 4)} (𝒬 u₁) (𝒬 u₂) := by        apply cdist_mono        apply ball_subset_ball        ring_nf        linarith      _ ≤ (2 ^ (a : ℝ)) ^ (6 : ℝ) * dist_{𝔠 p, (D ^ 𝔰 p / 4)} (𝒬 u₁) (𝒬 u₂) :=        mod_cast cdist_le_iterate (f := (𝒬 u₁)) (g := (𝒬 u₂)) (r := (D ^ (𝔰 p)) / 4)          (k := 6) (x := 𝔠 p) bigger    _ ≤ 2 ^ ((-(𝕔 - 6) : ℝ) * a) * 2 ^ ((Z : ℝ) * n / 2) := by      rcases hp with ⟨tile, notIn𝔖₀⟩      unfold 𝔖₀ at notIn𝔖₀      simp only [mem_setOf_eq, not_or, not_and, sep_union, mem_union] at notIn𝔖₀      gcongr      apply le_of_not_ge      exact notIn𝔖₀.2 tile