TileStructure.Forest.holder_correlation_tree

lemma holder_correlation_tree (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂) (h2u : 𝓘 u₁ ≤ 𝓘 u₂)    (hJ : J ∈ 𝓙₅ t u₁ u₂) (hf₁ : BoundedCompactSupport f₁) (hf₂ : BoundedCompactSupport f₂) :    iHolENorm (holderFunction t u₁ u₂ f₁ f₂ J) (c J) (16 * D ^ s J) τ ≤    C7_5_4 a * P7_5_4 t u₁ u₂ f₁ f₂ J := by  unfold iHolENorm  calc    _ ≤ C7_5_9s a * C7_5_10 a * P7_5_4 t u₁ u₂ f₁ f₂ J +        ENNReal.ofReal (16 * D ^ s J) ^ τ *        ⨆ x ∈ ball (c J) (16 * D ^ s J), ⨆ y ∈ ball (c J) (16 * D ^ s J), ⨆ (_ : x ≠ y),          (I7_5_4 a * P7_5_4 t u₁ u₂ f₁ f₂ J * ((D : ℝ≥0∞) ^ s J)⁻¹ ^ (a : ℝ)⁻¹) := by      gcongr with x mx x' mx' hn      · exact iSup₂_le_iff.mpr fun x mx ↦ enorm_holderFunction_le hu₁ hu₂ hu h2u hJ hf₁ hf₂ mx      · calc          _ ≤ I7_5_4 a * P7_5_4 t u₁ u₂ f₁ f₂ J *              (edist x x' / D ^ s J) ^ (a : ℝ)⁻¹ / edist x x' ^ τ := by              rw [← edist_eq_enorm_sub]              have h := edist_holderFunction_le hu₁ hu₂ hu h2u hJ hf₁ hf₂ mx mx'              exact ENNReal.div_le_div_right h (edist x x' ^ τ)          _ = _ := by            rw [mul_div_assoc, defaultτ, ← ENNReal.div_rpow_of_nonneg _ _ (by positivity),              div_eq_mul_inv, div_eq_mul_inv, ← mul_rotate _ (edist x x'),              ENNReal.inv_mul_cancel (by positivity [edist_pos.mpr hn]) (edist_ne_top x x'), one_mul]    _ ≤ C7_5_9s a * C7_5_10 a * P7_5_4 t u₁ u₂ f₁ f₂ J +        ENNReal.ofReal (16 * D ^ s J) ^ τ *        (I7_5_4 a * P7_5_4 t u₁ u₂ f₁ f₂ J * ((D : ℝ≥0∞) ^ s J)⁻¹ ^ (a : ℝ)⁻¹) := by      gcongr; exact iSup₂_le fun _ _ ↦ iSup₂_le fun _ _ ↦ iSup_le fun _ ↦ le_rfl    _ = (C7_5_9s a * C7_5_10 a + 16 ^ τ * I7_5_4 a) * P7_5_4 t u₁ u₂ f₁ f₂ J := by      have dn0 : ((D : ℝ≥0∞) ^ s J) ^ (a : ℝ)⁻¹ ≠ 0 := by        rw [← pos_iff_ne_zero]; refine ENNReal.rpow_pos_of_nonneg ?_ (by positivity)        exact ENNReal.zpow_pos (by unfold defaultD; positivity) (ENNReal.natCast_ne_top _) _      have dnt : ((D : ℝ≥0∞) ^ s J) ^ (a : ℝ)⁻¹ ≠ ⊤ := by        apply ENNReal.rpow_ne_top_of_nonneg (τ_nonneg X)        rw [← lt_top_iff_ne_top]        exact ENNReal.zpow_lt_top (by unfold defaultD; positivity) (ENNReal.natCast_ne_top _) _      rw [add_mul, ENNReal.ofReal_mul (by norm_num), ENNReal.ofReal_ofNat,        ENNReal.mul_rpow_of_nonneg _ _ (τ_nonneg X), ← Real.rpow_intCast,        ← ENNReal.ofReal_rpow_of_pos (realD_pos a), ENNReal.rpow_intCast, ENNReal.ofReal_natCast,        ← mul_assoc, ← mul_rotate _ (_ ^ _), mul_assoc _ (_ ^ τ), defaultτ, ENNReal.inv_rpow,        ENNReal.mul_inv_cancel dn0 dnt, mul_one, mul_rotate (_ ^ _)]    _ ≤ _ := by      gcongr      rw [show (16 : ℝ≥0∞) = (16 : ℝ≥0) by rfl, ← ENNReal.coe_rpow_of_nonneg _ (τ_nonneg X),        ← ENNReal.coe_mul, ← ENNReal.coe_mul, ← ENNReal.coe_add, ENNReal.coe_le_coe]      exact le_C7_5_4 (four_le_a X)