TileStructure.Forest.lower_oscillation_bound

lemma lower_oscillation_bound (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hJ : J ∈ 𝓙₅ t u₁ u₂) :    C7_5_11 a n ≤ dist_{c J, 8 * D ^ s J} (𝒬 u₁) (𝒬 u₂) := by  have existsBiggerThanJ : ∃ (J' : Grid X), J ≤ J' ∧ s J' = s J + 1 := by    apply Grid.exists_scale_succ    obtain ⟨⟨Jin𝓙₀, _⟩, ⟨jIsSubset : (J : Set X) ⊆ 𝓘 u₁, smaller : s J ≤ s (𝓘 u₁)⟩⟩ := hJ    obtain ⟨p, belongs⟩ := t.nonempty' hu₁    apply lt_of_le_of_ne smaller    by_contra! h    have u₁In𝓙₀ : 𝓘 u₁ ∈ 𝓙₀ (t.𝔖₀ u₁ u₂) := by      apply mem_of_eq_of_mem (h := Jin𝓙₀)      rw [eq_comm]      apply (eq_or_disjoint h).resolve_right      have notDisjoint := IF_subset_THEN_not_disjoint jIsSubset      rw [disjoint_comm] at notDisjoint      exact notDisjoint    cases u₁In𝓙₀ with    | inl min =>      have sameScale : s (𝓘 p) = s (𝓘 u₁) := by        linarith [          (scale_mem_Icc (i := 𝓘 p)).left,          show s (𝓘 p) ≤ s (𝓘 u₁) by exact (𝓘_le_𝓘 t hu₁ belongs).2        ]      suffices s (𝓘 u₁) > s (𝓘 p) by linarith      by_contra! smaller      have pIsSubset := (𝓘_le_𝓘 t hu₁ belongs).1      apply HasSubset.Subset.not_ssubset        ((fundamental_dyadic smaller).resolve_right (IF_subset_THEN_not_disjoint pIsSubset))      apply HasSubset.Subset.ssubset_of_ne pIsSubset      by_contra! sameSet      apply Forest.𝓘_ne_𝓘 (hu := hu₁) (hp := belongs)      exact Grid.inj (Prod.ext sameSet sameScale)    | inr avoidance =>      have pIn𝔖₀ : p ∈ t.𝔖₀ u₁ u₂ :=        𝔗_subset_𝔖₀ (hu₁ := hu₁) (hu₂ := hu₂) (hu := hu) (h2u := h2u) belongs      apply avoidance p pIn𝔖₀      calc (𝓘 p : Set X)      _ ⊆ 𝓘 u₁ := (𝓘_le_𝓘 t hu₁ belongs).1      _ ⊆ ball (c (𝓘 u₁)) (4 * D ^ s (𝓘 u₁)) := by        exact Grid_subset_ball      _ ⊆ ball (c (𝓘 u₁)) (100 * D ^ (s (𝓘 u₁) + 1)) := by        intro x hx        exact gt_trans (calculation_16 (X := X) (s := s (𝓘 u₁))) hx  rcases existsBiggerThanJ with ⟨J', JleJ', scaleSmaller⟩  have notIn𝓙₀ : J' ∉ 𝓙₀ (t.𝔖₀ u₁ u₂) := by    apply bigger_than_𝓙_is_not_in_𝓙₀ (sle := by linarith) (le := JleJ')    exact mem_of_mem_inter_left hJ  unfold 𝓙₀ at notIn𝓙₀  simp only [mem_setOf_eq, not_or, not_forall] at notIn𝓙₀  push Not at notIn𝓙₀  obtain ⟨_, ⟨ p, pIn, pSubset ⟩⟩ := notIn𝓙₀  have thus :=    calc 2 ^ ((Z : ℝ) * n / 2)    _ ≤ dist_{𝔠 p, D ^ 𝔰 p / 4} (𝒬 u₁) (𝒬 u₂) := pIn.2    _ ≤ dist_{c J, 128 * D^(s J + 2)} (𝒬 u₁) (𝒬 u₂) := by      apply cdist_mono      intro point pointIn      calc dist point (c J)      _ ≤ dist point (c J') + dist (c J') (c J) := dist_triangle ..      _ ≤ 100 * D ^ (s J' + 1) + dist (c J') (c J) := by        rw [ball, Set.subset_def] at pSubset        have := pSubset point (ball_subset_Grid pointIn)        rw [mem_setOf_eq] at this        gcongr      _ ≤ 100 * D ^ (s J' + 1) + 4 * D ^ (s J') := by        have : dist (c J) (c J') < 4 * D ^ (s J') :=          Grid.dist_c_le_of_subset (subset := JleJ'.1)        rw [dist_comm] at this        gcongr      _ = 100 * D ^ (s J + 2) + 4 * D ^ (s J + 1) := by        rw [scaleSmaller, add_assoc, show (1 : ℤ) + 1 = 2 by rfl]      _ < 128 * D^(s J + 2) := by        exact calculation_11 (s J) (X := X)    _ ≤ 2 ^ (2 * 𝕔 * (a^3) + 4 * a) * dist_{c J, 8 * D ^ s J} (𝒬 u₁) (𝒬 u₂) := by      rw [show 128 * (D : ℝ)^(s J + 2) = 2 ^ (2 * 𝕔 * a ^ 2 + 4) * (8*D^(s J))        by exact_mod_cast calculation_12 (s := s J)]      rw [calculation_13]      apply cdist_le_iterate      have := realD_pos a      positivity  rw [C7_5_11]  push_cast  linarith [calculation_14 (X := X) (n := n), calculation_15 thus]