TileStructure.Forest.holder_correlation_tree_1

lemma holder_correlation_tree_1 (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' ∈ 𝓘 u₁) :    edist (χ t u₁ u₂ J x) (χ t u₁ u₂ J x') *    ‖exp (.I * 𝒬 u₁ x) * adjointCarlesonSum (t u₁) f₁ x‖ₑ *    ‖exp (.I * 𝒬 u₂ x) * adjointCarlesonSum (t u₂ ∩ 𝔖₀ t u₁ u₂) f₂ x‖ₑ ≤    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) := by  simp_rw [enorm_mul, enorm_exp_I_mul_ofReal, one_mul]  by_cases mu₁ : x ∉ 𝓘 u₁  · have : adjointCarlesonSum (t u₁) f₁ x = 0 := by      refine Finset.sum_eq_zero fun p mp ↦ ?_      simp_rw [Finset.mem_filter_univ] at mp      rw [adjoint_tile_support2 hu₁ mp]      exact indicator_of_notMem mu₁ _    rw [this, enorm_zero, mul_zero, zero_mul]; exact zero_le  rw [not_not] at mu₁; rw [edist_dist]  calc    _ ≤ ENNReal.ofReal (C7_5_2 a * dist x x' / D ^ s J) *        ((⨅ x ∈ ball (c J) (8⁻¹ * D ^ s J), ‖adjointCarlesonSum (t u₁) f₁ x‖ₑ) +          C7_5_9s a * ⨅ x ∈ J, maximalFunction volume 𝓑 c𝓑 r𝓑 1 f₁ x) *        ((⨅ x ∈ ball (c J) (8⁻¹ * D ^ s J), ‖adjointCarlesonSum (t u₂) f₂ x‖ₑ) +          C7_5_10 a * ⨅ x ∈ J, maximalFunction volume 𝓑 c𝓑 r𝓑 1 f₂ x) := by      gcongr      · exact dist_χ_le hu₁ hu₂ hu h2u hJ mu₁ mx'      · exact (le_biSup _ mx).trans <|          global_tree_control1_supbound hu₁ hu₂ hu h2u _ (.inl rfl) hJ hf₁      · exact (le_biSup _ mx).trans <| global_tree_control2 hu₁ hu₂ hu h2u hJ hf₂    _ ≤ ENNReal.ofReal (C7_5_2 a * dist x x' / D ^ s J) *        (C7_5_9s a * C7_5_10 a * P7_5_4 t u₁ u₂ f₁ f₂ J) := by      rw [mul_assoc (ENNReal.ofReal _)]; gcongr _ * ?_      rw [P7_5_4, mul_mul_mul_comm]      conv_rhs => rw [mul_add, mul_add]      gcongr <;> (nth_rw 1 [← one_mul (⨅ x ∈ _, _)]; gcongr; rw [ENNReal.one_le_coe_iff])      · exact one_le_C7_5_9s      · exact one_le_C7_5_10 (four_le_a X)    _ = _ := by      rw [mul_div_assoc, ENNReal.ofReal_mul (by positivity), ENNReal.ofReal_coe_nnreal,        ENNReal.ofReal_div_of_pos (by unfold defaultD; positivity), ← edist_dist x x',        ← Real.rpow_intCast, ← ENNReal.ofReal_rpow_of_pos (realD_pos a), ENNReal.rpow_intCast,        ENNReal.ofReal_natCast]      ring