TileStructure.Forest.enorm_holderFunction_le

lemma enorm_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)) :    ‖holderFunction t u₁ u₂ f₁ f₂ J x‖ₑ ≤ C7_5_9s a * C7_5_10 a * P7_5_4 t u₁ u₂ f₁ f₂ J := by  simp_rw [holderFunction, enorm_mul, RCLike.enorm_conj, enorm_mul, enorm_exp_I_mul_ofReal, one_mul,    Complex.enorm_real, NNReal.enorm_eq]  calc    _ ≤ 1 * (⨆ z ∈ ball (c J) (16 * D ^ s J), ‖adjointCarlesonSum (t u₁) f₁ z‖ₑ) *        ⨆ z ∈ ball (c J) (16 * D ^ s J), ‖adjointCarlesonSum (t u₂ ∩ 𝔖₀ t u₁ u₂) f₂ z‖ₑ := by      gcongr      · rw [ENNReal.coe_le_one_iff]        exact (χ_le_indicator hJ).trans ((indicator_le fun _ _ ↦ le_refl _) _)      · apply le_biSup _ mx      · apply le_biSup _ mx    _ ≤ ((⨅ 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      rw [one_mul]; gcongr      · exact global_tree_control1_supbound hu₁ hu₂ hu h2u _ (.inl rfl) hJ hf₁      · exact global_tree_control2 hu₁ hu₂ hu h2u hJ hf₂    _ ≤ _ := by      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)