TileStructure.Forest.cdtp_le_iHolENorm

lemma cdtp_le_iHolENorm (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hf₁ : BoundedCompactSupport f₁) (hf₂ : BoundedCompactSupport f₂) :    ‖∫ x, adjointCarlesonSum (t u₁) f₁ x * conj (adjointCarlesonSum (t u₂ ∩ 𝔖₀ t u₁ u₂) f₂ x)‖ₑ ≤    ∑ J ∈ 𝓙₅ t u₁ u₂, C2_0_5 a * volume (ball (c J) (8 * D ^ s J)) *      iHolENorm (holderFunction t u₁ u₂ f₁ f₂ J) (c J) (2 * (8 * D ^ s J)) τ *      (1 + edist_{c J, 8 * D ^ s J} (𝒬 u₂) (𝒬 u₁)) ^ (-(2 * a^2 + a^3 : ℝ)⁻¹) := by  classical  have rearr : ∀ J x, t.χ u₁ u₂ J x *      (adjointCarlesonSum (t u₁) f₁ x * conj (adjointCarlesonSum (t u₂ ∩ 𝔖₀ t u₁ u₂) f₂ x)) =      exp (I * (𝒬 u₂ x - 𝒬 u₁ x)) * holderFunction t u₁ u₂ f₁ f₂ J x := fun J x ↦ by    unfold holderFunction    simp_rw [map_mul, ← mul_assoc]; congr 1    rw [← mul_rotate _ _ (adjointCarlesonSum _ _ _)]; congr 1    rw [← exp_conj, map_mul, conj_I, conj_ofReal, ← mul_assoc, ← mul_assoc, ← Complex.exp_add,      neg_mul, ← sub_eq_neg_add, ← mul_sub, sub_sub_cancel_left, ← mul_rotate, ← Complex.exp_add,      ← mul_add, add_neg_cancel, mul_zero, exp_zero, one_mul]  calc    _ = ‖∫ x in 𝓘 u₁, adjointCarlesonSum (t u₁) f₁ x *        conj (adjointCarlesonSum (t u₂ ∩ 𝔖₀ t u₁ u₂) f₂ x)‖ₑ := by      congr 1; refine (setIntegral_eq_integral_of_forall_compl_eq_zero fun x nx ↦ ?_).symm      rw [adjoint_tile_support2_sum hu₁, indicator_of_notMem nx, zero_mul]    _ = ‖∑ J ∈ 𝓙₅ t u₁ u₂, ∫ x, χ t u₁ u₂ J x * (adjointCarlesonSum (t u₁) f₁ x *        conj (adjointCarlesonSum (t u₂ ∩ 𝔖₀ t u₁ u₂) f₂ x))‖ₑ := by      rw [← integral_indicator coeGrid_measurable]      conv_lhs =>        enter [1, 2, x]        rw [indicator_eq_indicator_one_mul, show (1 : X → ℂ) = (↑) ∘ (1 : X → ℝ≥0) by rfl,          indicator_comp_of_zero (by simp), Function.comp_apply, ← sum_χ hu₁ hu₂ hu h2u x,          NNReal.coe_sum, ofReal_sum, Finset.sum_mul]      congr 1      refine integral_finsetSum _ fun J mJ ↦ ((BoundedCompactSupport.toComplex ?_).mul        (hf₁.adjointCarlesonSum.mul hf₂.adjointCarlesonSum.conj)).integrable      rw [mem_toFinset] at mJ; exact boundedCompactSupport_toReal_χ mJ    _ ≤ ∑ J ∈ 𝓙₅ t u₁ u₂, ‖∫ x, χ t u₁ u₂ J x * (adjointCarlesonSum (t u₁) f₁ x *        conj (adjointCarlesonSum (t u₂ ∩ 𝔖₀ t u₁ u₂) f₂ x))‖ₑ := enorm_sum_le _ _    _ = ∑ J ∈ 𝓙₅ t u₁ u₂,        ‖∫ x, exp (.I * (𝒬 u₂ x - 𝒬 u₁ x)) * holderFunction t u₁ u₂ f₁ f₂ J x‖ₑ := by      congr! 4 with J mJ x; exact rearr ..    _ ≤ _ := by      gcongr with J mJ; apply holder_van_der_corput (X := X); rw [support_subset_iff']; intro x nx      rw [mem_toFinset] at mJ      rw [holderFunction, χ_eq_zero_of_notMem_ball mJ nx, NNReal.coe_zero, ofReal_zero, zero_mul,        zero_mul]