TileStructure.Forest.global_tree_control1_supbound

lemma global_tree_control1_supbound (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (ℭ : Set (𝔓 X)) (hℭ : ℭ = t u₁ ∨ ℭ = t u₂ ∩ 𝔖₀ t u₁ u₂)    (hJ : J ∈ 𝓙₅ t u₁ u₂) (hf : BoundedCompactSupport f) :    ⨆ x ∈ ball (c J) (16 * D ^ s J), ‖adjointCarlesonSum ℭ f x‖ₑ ≤    (⨅ x ∈ ball (c J) (8⁻¹ * D ^ s J), ‖adjointCarlesonSum ℭ f x‖ₑ) +    C7_5_9s a * ⨅ x ∈ J, maximalFunction volume 𝓑 c𝓑 r𝓑 1 f x := by  rw [← tsub_le_iff_left]; refine ENNReal.le_of_forall_pos_le_add fun ε εpos blt ↦ ?_  obtain ⟨x, hx, ex⟩ : ∃ x₀ ∈ ball (c J) (16 * D ^ s J),      ⨆ x ∈ ball (c J) (16 * D ^ s J), ‖adjointCarlesonSum ℭ f x‖ₑ ≤      ‖adjointCarlesonSum ℭ f x₀‖ₑ + (ε / 2 : ℝ≥0) := by    apply ENNReal.exists_biSup_le_enorm_add_eps (by positivity)      ⟨c J, mem_ball_self (by unfold defaultD; positivity)⟩    rw [isBounded_image_iff_bddAbove_norm']    exact hf.bddAbove_norm_adjointCarlesonSum |>.mono (image_subset_range ..)  obtain ⟨x', hx', ex'⟩ : ∃ x₀ ∈ ball (c J) (8⁻¹ * D ^ s J),      ‖adjointCarlesonSum ℭ f x₀‖ₑ - (ε / 2 : ℝ≥0) ≤      ⨅ x ∈ ball (c J) (8⁻¹ * D ^ s J), ‖adjointCarlesonSum ℭ f x‖ₑ :=    ENNReal.exists_enorm_sub_eps_le_biInf (by positivity)      ⟨c J, mem_ball_self (by unfold defaultD; positivity)⟩  calc    _ ≤ (‖adjointCarlesonSum ℭ f x‖ₑ + (ε / 2 : ℝ≥0)) -        (‖adjointCarlesonSum ℭ f x'‖ₑ - (ε / 2 : ℝ≥0)) := tsub_le_tsub ex ex'    _ ≤ (ε / 2 : ℝ≥0) + ‖adjointCarlesonSum ℭ f x‖ₑ -        ‖adjointCarlesonSum ℭ f x'‖ₑ + (ε / 2 : ℝ≥0) := by      rw [add_comm]; exact tsub_tsub_le_tsub_add    _ ≤ (ε / 2 : ℝ≥0) + (‖adjointCarlesonSum ℭ f x‖ₑ - ‖adjointCarlesonSum ℭ f x'‖ₑ) +        (ε / 2 : ℝ≥0) := add_le_add_left add_tsub_le_assoc _    _ = ‖‖adjointCarlesonSum ℭ f x‖ₑ - ‖adjointCarlesonSum ℭ f x'‖ₑ‖ₑ + ε := by      rw [add_rotate, add_assoc]; simp    _ ≤ (C7_5_9d a * (edist x x' / D ^ s J) ^ (a : ℝ)⁻¹ * ⨅ x ∈ J, maximalFunction volume 𝓑 c𝓑 r𝓑 1 f x) + ε := by      refine add_le_add_left ?_ _      replace hx' : x' ∈ ball (c J) (16 * D ^ s J) := by        exact (ball_subset_ball (by gcongr; norm_num)) hx'      rcases hℭ with rfl | rfl      · nth_rw 2 [← one_mul ‖_‖ₑ]; rw [← enorm_exp_I_mul_ofReal (𝒬 u₁ x), ← enorm_mul]        nth_rw 3 [← one_mul ‖_‖ₑ]; rw [← enorm_exp_I_mul_ofReal (𝒬 u₁ x'), ← enorm_mul]        apply ENNReal.enorm_enorm_sub_enorm_le.trans        rw [← edist_eq_enorm_sub]        exact global_tree_control1_edist_left hu₁ hu₂ hu h2u hJ hf hx hx'      · nth_rw 2 [← one_mul ‖_‖ₑ]; rw [← enorm_exp_I_mul_ofReal (𝒬 u₂ x), ← enorm_mul]        nth_rw 3 [← one_mul ‖_‖ₑ]; rw [← enorm_exp_I_mul_ofReal (𝒬 u₂ x'), ← enorm_mul]        apply ENNReal.enorm_enorm_sub_enorm_le.trans        rw [← edist_eq_enorm_sub]        exact global_tree_control1_edist_right hu₁ hu₂ hu h2u hJ hf hx hx'    _ ≤ (C7_5_9d a * 2 ^ ((2 : ℕ) : ℝ) * ⨅ x ∈ J, maximalFunction volume 𝓑 c𝓑 r𝓑 1 f x) + ε := by      gcongr; rw [mem_ball] at hx hx'; rw [edist_dist]      calc        _ ≤ (ENNReal.ofReal ((16 + 8⁻¹) * D ^ s J) / D ^ s J) ^ (a : ℝ)⁻¹ := by          gcongr; rw [add_mul]; exact ((dist_triangle_right ..).trans_lt (add_lt_add hx hx')).le        _ ≤ (2 ^ (8 : ℝ)) ^ (a : ℝ)⁻¹ := by          have Dpos : 0 < (D : ℝ≥0∞) ^ s J := ENNReal.zpow_pos (by simp) (by simp) _          have Dlt : (D : ℝ≥0∞) ^ s J < ⊤ := ENNReal.zpow_lt_top (by simp) (by simp) _          rw [ENNReal.ofReal_mul (by norm_num), ← Real.rpow_intCast,            ← ENNReal.ofReal_rpow_of_pos (by unfold defaultD; positivity),            show ENNReal.ofReal D = D by norm_cast, ENNReal.rpow_intCast,            ENNReal.mul_div_cancel_right Dpos.ne' Dlt.ne]          exact ENNReal.rpow_le_rpow (by norm_num) (by positivity)        _ ≤ (2 ^ (8 : ℝ)) ^ (4 : ℝ)⁻¹ := by          gcongr; exacts [by norm_num, by norm_cast; linarith [four_le_a X]]        _ = _ := by rw [← ENNReal.rpow_mul]; norm_num    _ = _ := by      congr      rw [C7_5_9d, C7_5_9s, ENNReal.coe_mul, ENNReal.coe_pow, ENNReal.coe_ofNat, mul_assoc,        ENNReal.rpow_natCast, ← pow_add]; rfl