TileStructure.Forest.dist_χ_le

lemma dist_χ_le (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hJ : J ∈ 𝓙₅ t u₁ u₂) (mx : x ∈ 𝓘 u₁) (mx' : x' ∈ 𝓘 u₁) :    dist (χ t u₁ u₂ J x) (χ t u₁ u₂ J x') ≤ C7_5_2 a * dist x x' / D ^ s J := by  classical  by_cases hxx : x ∉ ball (c J) (8 * D ^ s J) ∧ x' ∉ ball (c J) (8 * D ^ s J)  · have n₁ := χ_le_indicator hJ (x := x)    rw [indicator_of_notMem hxx.1, nonpos_iff_eq_zero] at n₁    have n₂ := χ_le_indicator hJ (x := x')    rw [indicator_of_notMem hxx.2, nonpos_iff_eq_zero] at n₂    rw [n₁, n₂, dist_self]; positivity  rw [not_and_or, not_notMem, not_notMem] at hxx  wlog hx : x ∈ ball (c J) (8 * D ^ s J) generalizing x x'  · rw [or_comm] at hxx; specialize this mx' mx hxx (hxx.resolve_right hx)    rwa [dist_comm, dist_comm x' x] at this  clear hxx  let ctx := χtilde J u₁ x  let ctx' := χtilde J u₁ x'  let ax := ∑ J' ∈ 𝓙₅ t u₁ u₂, χtilde J' u₁ x  let ax' := ∑ J' ∈ 𝓙₅ t u₁ u₂, χtilde J' u₁ x'  have ax4 : 4 ≤ ax := (four_lt_sum_χtilde hu₁ hu₂ hu h2u mx).le  have ax'4 : 4 ≤ ax' := (four_lt_sum_χtilde hu₁ hu₂ hu h2u mx').le  have nax : (ax : ℝ) ≠ 0 := by exact_mod_cast (zero_lt_four.trans_le ax4).ne'  have nax' : (ax' : ℝ) ≠ 0 := by exact_mod_cast (zero_lt_four.trans_le ax'4).ne'  have part1 : dist (χ t u₁ u₂ J x) (χ t u₁ u₂ J x') ≤      (dist x x' / D ^ s J + ctx' * dist ax ax') / 4 := by    calc      _ = ‖(ctx - ctx' : ℝ) / ax - ctx' * (ax - ax') / (ax * ax')‖ := by        rw [mul_sub, sub_div, sub_div, mul_div_mul_right _ _ nax', mul_comm (ax : ℝ) ax',          mul_div_mul_right _ _ nax, ← sub_add, sub_right_comm, sub_add_cancel]; rfl      _ ≤ dist ctx ctx' / ax + ctx' * dist ax ax' / (ax * ax') := by        change _ ≤ ‖(ctx - ctx' : ℝ)‖ / ax + ctx' * ‖(ax - ax' : ℝ)‖ / (ax * ax')        conv_rhs => enter [1]; rw [← NNReal.norm_eq ax]        conv_rhs =>          enter [2]; rw [← NNReal.norm_eq ctx']          enter [2]; rw [← NNReal.norm_eq ax, ← NNReal.norm_eq ax']        rw [← norm_mul, ← norm_mul, ← norm_div, ← norm_div]        exact nnnorm_sub_le ..      _ ≤ dist ctx ctx' / 4 + ctx' * dist ax ax' / (1 * 4) := by        gcongr <;> norm_cast; exact le_trans (by norm_num) ax4      _ ≤ _ := by        rw [one_mul, ← add_div]; gcongr; exact dist_χtilde_le mx mx'  apply part1.trans  by_cases hx' : x' ∉ ball (c J) (8 * D ^ s J)  · have : ctx' = 0 := by      simp_rw [ctx', ← not_ne_iff, ← zero_lt_iff, χtilde_pos_iff]; tauto    rw [this, NNReal.coe_zero, zero_mul, add_zero, div_eq_inv_mul _ 4, mul_div_assoc]; gcongr    rw [show 4⁻¹ = (2 : ℝ) ^ (-2 : ℝ) by norm_num, C7_5_2, NNReal.coe_pow, NNReal.coe_ofNat,      ← Real.rpow_natCast, Real.rpow_le_rpow_left_iff one_lt_two]    apply le_trans ?_ (by positivity)    linarith  rw [not_notMem] at hx'  calc    _ ≤ (dist x x' / D ^ s J +        8 * ∑ J' ∈ 𝓙₅ t u₁ u₂, dist (χtilde J' u₁ x) (χtilde J' u₁ x')) / 4 := by      gcongr      · exact χtilde_le_eight      · have := dist_sum_sum_le (𝓙₅ t u₁ u₂).toFinset          (fun J' ↦ (χtilde J' u₁ x : ℝ)) (fun J' ↦ χtilde J' u₁ x')        exact_mod_cast this    _ = (dist x x' / D ^ s J +        8 * ∑ J' ∈ 𝓙₅ t u₁ u₂ with          ¬Disjoint (ball (c J) (8 * D ^ s J)) (ball (c J') (8 * D ^ s J')),            dist (χtilde J' u₁ x) (χtilde J' u₁ x')) / 4 := by      congr 3; refine (Finset.sum_filter_of_ne fun J' mJ' hd ↦ ?_).symm; contrapose! hd      have h₁ : χtilde J' u₁ x = 0 := by        have := disjoint_left.mp hd hx        rw [← not_ne_iff, ← zero_lt_iff, χtilde_pos_iff]; tauto      have h₂ : χtilde J' u₁ x' = 0 := by        have := disjoint_left.mp hd hx'        rw [← not_ne_iff, ← zero_lt_iff, χtilde_pos_iff]; tauto      rw [h₁, h₂, dist_self]    _ ≤ (dist x x' / D ^ s J +        8 * ∑ J' ∈ 𝓙₅ t u₁ u₂ with          ¬Disjoint (ball (c J) (8 * D ^ s J)) (ball (c J') (8 * D ^ s J')),            dist x x' * D ^ (1 - s J)) / 4 := by      gcongr with J' mJ'; trans dist x x' / D ^ (s J')      · exact dist_χtilde_le mx mx'      · rw [div_eq_mul_inv, ← zpow_neg]; gcongr        · exact one_le_realD a        · rw [Finset.mem_filter, mem_toFinset] at mJ'          rw [neg_le, neg_sub]; exact moderate_scale_change hJ mJ'.1 mJ'.2    _ = dist x x' / (D : ℝ) ^ s J *        (1 / 4 + 2 * D * {J' ∈ (𝓙₅ t u₁ u₂).toFinset |          ¬Disjoint (ball (c J) (8 * D ^ s J)) (ball (c J') (8 * D ^ s J'))}.card) := by      rw [Finset.sum_const, nsmul_eq_mul, zpow_sub₀ (by simp), zpow_one,        show 8 * (_ * (dist x x' * (D / D ^ s J))) = dist x x' / D ^ s J * (2 * D * _) * 4 by ring,        add_div, mul_div_cancel_right₀ _ four_ne_zero, div_eq_mul_one_div, ← mul_add]    _ ≤ _ := by rw [mul_comm, mul_div_assoc]; gcongr; exact quarter_add_two_mul_D_mul_card_le hJ