TileStructure.Forest.edist_holderFunction_le

lemma edist_holderFunction_le (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂) (h2u : 𝓘 u₁ ≤ 𝓘 u₂)    (hJ : J ∈ 𝓙₅ t u₁ u₂) (hf₁ : BoundedCompactSupport f₁) (hf₂ : BoundedCompactSupport f₂)    (mx : x ∈ ball (c J) (16 * D ^ s J)) (mx' : x' ∈ ball (c J) (16 * D ^ s J)) :    edist (holderFunction t u₁ u₂ f₁ f₂ J x) (holderFunction t u₁ u₂ f₁ f₂ J x') ≤    I7_5_4 a * P7_5_4 t u₁ u₂ f₁ f₂ J * (edist x x' / D ^ s J) ^ (a : ℝ)⁻¹ := by  by_cases mu₁ : x ∉ 𝓘 u₁ ∧ x' ∉ 𝓘 u₁  · have h0 := support_subset_iff'.mp (support_holderFunction_subset u₂ f₁ f₂ J hu₁)    rw [h0 _ mu₁.1, h0 _ mu₁.2, edist_self]; exact zero_le  rw [not_and_or, not_not, not_not] at mu₁  wlog mu₁' : x' ∈ 𝓘 u₁ generalizing x x'  · specialize this mx' mx mu₁.symm (mu₁.resolve_right mu₁')    rwa [edist_comm, edist_comm x'] at this  let CH := χ t u₁ u₂ J  let T₁ := fun z ↦ exp (.I * 𝒬 u₁ z) * adjointCarlesonSum (t u₁) f₁ z  let T₂ := fun z ↦ exp (.I * 𝒬 u₂ z) * adjointCarlesonSum (t u₂ ∩ 𝔖₀ t u₁ u₂) f₂ z  rw [edist_eq_enorm_sub]  change ‖CH x * T₁ x * conj (T₂ x) - CH x' * T₁ x' * conj (T₂ x')‖ₑ ≤ _  calc    _ ≤ edist (CH x * T₁ x * conj (T₂ x)) (CH x' * T₁ x * conj (T₂ x)) +        edist (CH x' * T₁ x * conj (T₂ x)) (CH x' * T₁ x' * conj (T₂ x)) +        edist (CH x' * T₁ x' * conj (T₂ x)) (CH x' * T₁ x' * conj (T₂ x')) := by      rw [← edist_eq_enorm_sub]      exact edist_triangle4 ..    _ = edist (CH x) (CH x') * ‖T₁ x‖ₑ * ‖T₂ x‖ₑ + CH x' * edist (T₁ x) (T₁ x') * ‖T₂ x‖ₑ +        CH x' * ‖T₁ x'‖ₑ * edist (T₂ x) (T₂ x') := by      simp_rw [edist_eq_enorm_sub, ← sub_mul, ← mul_sub, ← map_sub (starRingEnd ℂ), enorm_mul, RCLike.enorm_conj]      rw [Complex.enorm_real, NNReal.enorm_eq, edist_dist, NNReal.dist_eq, ← Complex.ofReal_sub, Complex.enorm_real, Real.enorm_eq_ofReal_abs]    _ ≤ C7_5_2 a * C7_5_9s a * C7_5_10 a * P7_5_4 t u₁ u₂ f₁ f₂ J * (edist x x' / D ^ s J) +        C7_5_9d a * C7_5_10 a * P7_5_4 t u₁ u₂ f₁ f₂ J * (edist x x' / D ^ s J) ^ (a : ℝ)⁻¹ +        C7_5_9s a * C7_5_9d a * P7_5_4 t u₁ u₂ f₁ f₂ J * (edist x x' / D ^ s J) ^ (a : ℝ)⁻¹ := by      gcongr ?_ + ?_ + ?_      · exact holder_correlation_tree_1 hu₁ hu₂ hu h2u hJ hf₁ hf₂ mx mu₁'      · exact holder_correlation_tree_2 hu₁ hu₂ hu h2u hJ hf₁ hf₂ mx mx'      · exact holder_correlation_tree_3 hu₁ hu₂ hu h2u hJ hf₁ hf₂ mx mx'    _ ≤ C7_5_2 a * C7_5_9s a * C7_5_10 a * P7_5_4 t u₁ u₂ f₁ f₂ J *          (32 * (edist x x' / D ^ s J) ^ (a : ℝ)⁻¹) +        C7_5_9d a * C7_5_10 a * P7_5_4 t u₁ u₂ f₁ f₂ J * (edist x x' / D ^ s J) ^ (a : ℝ)⁻¹ +        C7_5_9s a * C7_5_9d a * P7_5_4 t u₁ u₂ f₁ f₂ J * (edist x x' / D ^ s J) ^ (a : ℝ)⁻¹ := by      gcongr      rcases le_or_gt (edist x x' / D ^ s J) 1 with h | h      · nth_rw 1 [← one_mul (_ / _), ← ENNReal.rpow_one (_ / _)]        refine mul_le_mul' (by norm_num) (ENNReal.rpow_le_rpow_of_exponent_ge h ?_)        rw [inv_le_one_iff₀]; right; exact_mod_cast a_pos X      · nth_rw 1 [← mul_one (_ / _), ← ENNReal.one_rpow (a : ℝ)⁻¹]        refine mul_le_mul' (ENNReal.div_le_of_le_mul ?_) (ENNReal.rpow_le_rpow h.le (by positivity))        have hc : 32 * (D : ℝ≥0∞) ^ s J = ENNReal.ofReal (32 * D ^ s J) := by          rw [ENNReal.ofReal_mul (by norm_num), ← Real.rpow_intCast,            ← ENNReal.ofReal_rpow_of_pos (realD_pos a), ENNReal.rpow_intCast,            ENNReal.ofReal_natCast, ENNReal.ofReal_ofNat]        rw [edist_dist, hc]; apply ENNReal.ofReal_le_ofReal        calc          _ ≤ dist x (c J) + dist x' (c J) := dist_triangle_right ..          _ ≤ 16 * D ^ s J + 16 * D ^ s J := add_le_add (mem_ball.mp mx).le (mem_ball.mp mx').le          _ = _ := by ring    _ = (32 * C7_5_2 a * C7_5_9s a * C7_5_10 a + C7_5_9d a * C7_5_10 a + C7_5_9s a * C7_5_9d a)          * P7_5_4 t u₁ u₂ f₁ f₂ J * (edist x x' / D ^ s J) ^ (a : ℝ)⁻¹ := by ring    _ ≤ _ := by      gcongr      norm_cast      apply le_I7_5_4 (four_le_a X)