Holder van der corput

theorem holder_van_der_corput {z : X} {R : ℝ} {φ : X → ℂ}    (φ_supp : support φ ⊆ ball z R) {f g : Θ X} :    ‖∫ x, exp (I * (f x - g x)) * φ x‖ₑ ≤    (C2_0_5 a : ℝ≥0∞) * volume (ball z R) * iHolENorm φ z (2 * R) τ *      (1 + edist_{z, R} f g) ^ (- (2 * a^2 + a^3 : ℝ)⁻¹) := by  have : 4 ≤ a := four_le_a X  have : (4 : ℝ) ≤ a := mod_cast four_le_a X  rcases le_or_gt R 0 with hR | hR  · simp [ball_eq_empty.2 hR, subset_empty_iff, support_eq_empty_iff] at φ_supp    simp [φ_supp]  rcases eq_or_ne (iHolENorm φ z (2 * R) τ) ∞ with h2φ | h2φ  · apply le_top.trans_eq    symm    simp only [defaultτ] at h2φ    have : (0 : ℝ) < 2 * a ^ 2 + a ^ 3 := by positivity    simp [h2φ, C2_0_5, (measure_ball_pos volume z hR).ne', this, edist_ne_top]  let t : ℝ := (1 + nndist_{z, R} f g) ^ (- (τ / (2 + a)))  have t_pos : 0 < t := Real.rpow_pos_of_pos (by positivity) _  have t_one : t ≤ 1 := by    apply Real.rpow_le_one_of_one_le_of_nonpos    · simp only [le_add_iff_nonneg_right,  NNReal.zero_le_coe]    · simp only [defaultτ, Left.neg_nonpos_iff]      positivity  have φ_cont : Continuous φ := continuous_of_iHolENorm_ne_top' (τ_pos X) φ_supp h2φ  have φ_comp : HasCompactSupport φ := by    apply HasCompactSupport.of_support_subset_isCompact (isCompact_closedBall z R)    exact φ_supp.trans ball_subset_closedBall  let φ' := holderApprox R t φ  have φ'_supp : support φ' ⊆ ball z (2 * R) := support_holderApprox_subset hR φ_supp ⟨t_pos, t_one⟩  have φ'_cont : Continuous φ' := by    apply LipschitzWith.continuous    apply lipschitzWith_holderApprox hR t_pos t_one φ_cont φ_supp    exact fun x ↦ norm_le_iHolNNNorm_of_subset h2φ (φ_supp.trans (ball_subset_ball (by linarith)))  have φ'_comp : HasCompactSupport φ' := by    apply HasCompactSupport.of_support_subset_isCompact (isCompact_closedBall z (2 * R))    exact φ'_supp.trans ball_subset_closedBall  have : volume (ball z (2 * R)) ≤ 2 ^ a * volume (ball z R) := by    convert measure_ball_two_le_same z R (μ := volume)    simp [defaultA]  /- First step: control `‖∫ x, exp (I * (f x - g x)) * φ' x‖ₑ`, using that this function is  Lipschitz and the cancellativity assumption for the integral against Lipschitz functions. -/  have : (ENNReal.ofReal t) ^ (-1 - a : ℝ) * (1 + edist_{z, R} f g) ^ (- τ) ≤      (1 + edist_{z, R} f g) ^ (- τ ^ 2 / (2 + a)) := by    simp only [coe_nndist, defaultτ, t]    rw [← ENNReal.ofReal_rpow_of_pos (by positivity),      ENNReal.ofReal_add zero_le_one (by positivity), ← edist_dist, ENNReal.ofReal_one]    rw [← ENNReal.rpow_mul, ← ENNReal.rpow_add]; rotate_left    · apply ne_of_gt      apply zero_lt_one.trans_le (by simp)    · simp [edist_ne_top]    gcongr    · simp    · field_simp      nlinarith  have : ‖∫ x, exp (I * (f x - g x)) * φ' x‖ₑ ≤ 2 ^ (6 * a) * volume (ball z R)        * iHolENorm φ z (2 * R) τ * (1 + edist_{z, R} f g) ^ (- τ ^ 2 / (2 + a)) := calc      ‖∫ x, exp (I * (f x - g x)) * φ' x‖ₑ    _ ≤ 2 ^ a * volume (ball z (2 * R))      * iLipENorm φ' z (2 * R) * (1 + edist_{z, 2 * R} f g) ^ (- τ) := by      simpa only [defaultA, Nat.cast_pow, Nat.cast_ofNat, t] using        enorm_integral_exp_le (x := z) (r := 2 * R) (φ := φ') φ'_supp (f := f) (g := g)    _ ≤ 2 ^ a * (2 ^ a * volume (ball z R))        * (2 ^ (4 * a) * (ENNReal.ofReal t) ^ (-1 - a : ℝ) * iHolENorm φ z (2 * R) τ)        * (1 + edist_{z, R} f g) ^ (- τ) := by      gcongr 2 ^ a * ?_ * ?_ * ?_      · exact iLipENorm_holderApprox_le t_pos t_one φ_supp      · apply ENNReal.rpow_le_rpow_of_nonpos        · simp        apply add_le_add_right        simp only [edist_dist]        apply ENNReal.ofReal_le_ofReal        apply CompatibleFunctions.cdist_mono        apply ball_subset_ball (by linarith)    _ = 2 ^ (6 * a) * volume (ball z R) * iHolENorm φ z (2 * R) τ *        ((ENNReal.ofReal t) ^ (-1 - a : ℝ) * (1 + edist_{z, R} f g) ^ (- τ)) := by      rw [show 6 * a = 4 * a + a + a by ring, pow_add, pow_add]      ring    _ ≤ 2 ^ (6 * a) * volume (ball z R) * iHolENorm φ z (2 * R) τ *        (1 + edist_{z, R} f g) ^ (- τ ^ 2 / (2 + a)) := by gcongr;  /- Second step: control `‖∫ x, exp (I * (f x - g x)) * (φ x - φ' x)‖ₑ` using that `‖φ x - φ' x‖`  is controlled pointwise, and vanishes outside of `B (z, 2R)`. -/  have : ENNReal.ofReal (t/2) ^ τ ≤ (1 + edist_{z, R} f g) ^ (- τ ^ 2 / (2 + a)) := by    have : 0 < τ := τ_pos X    have : ENNReal.ofReal (t/2) ^ τ ≤ ENNReal.ofReal t ^ τ := by gcongr; linarith    apply this.trans_eq    rw [show - τ ^ 2 / (2 + a) = (-τ / (2 + a)) * τ by ring, ENNReal.rpow_mul]    congr 1    simp only [coe_nndist, defaultτ, t]    rw [← ENNReal.ofReal_rpow_of_pos (by positivity),      ENNReal.ofReal_add zero_le_one (by positivity), ← edist_dist, ENNReal.ofReal_one]    congr    ring  have : ‖∫ x, exp (I * (f x - g x)) * (φ x - φ' x)‖ₑ    ≤ 2 ^ (6 * a) * volume (ball z R) * iHolENorm φ z (2 * R) τ *        (1 + edist_{z, R} f g) ^ (- τ ^ 2 / (2 + a)) := calc      ‖∫ x, exp (I * (f x - g x)) * (φ x - φ' x)‖ₑ    _ = ‖∫ x in ball z (2 * R), exp (I * (f x - g x)) * (φ x - φ' x)‖ₑ := by      rw [setIntegral_eq_integral_of_forall_compl_eq_zero]      intro x hx      have A : φ x = 0 := by        apply notMem_support.1        contrapose! hx        apply (φ_supp.trans (ball_subset_ball (by linarith))) hx      have A' : φ' x = 0 := by        apply notMem_support.1        contrapose! hx        apply φ'_supp hx      simp [A, A']    _ ≤ ∫⁻ x in ball z (2 * R), ‖exp (I * (f x - g x)) * (φ x - φ' x)‖ₑ :=      enorm_integral_le_lintegral_enorm _    _ = ∫⁻ x in ball z (2 * R), ‖φ x - φ' x‖ₑ := by      simp only [enorm_mul, ← ofReal_sub, enorm_exp_I_mul_ofReal, one_mul]    _ ≤ ∫⁻ x in ball z (2 * R), ENNReal.ofReal (t/2) ^ τ * iHolENorm φ z (2 * R) τ :=      lintegral_mono (fun x ↦ enorm_holderApprox_sub_le hR t_pos t_one φ_supp x)    _ = volume (ball z (2 * R)) * ENNReal.ofReal (t/2) ^ τ * iHolENorm φ z (2 * R) τ := by      simp; ring    _ ≤ (2 ^ a * volume (ball z R)) * ENNReal.ofReal (t/2) ^ τ * iHolENorm φ z (2 * R) τ := by      gcongr    _ = 2 ^ a * volume (ball z R) * iHolENorm φ z (2 * R) τ * ENNReal.ofReal (t/2) ^ τ := by ring    _ ≤ 2 ^ (6 * a) * volume (ball z R) * iHolENorm φ z (2 * R) τ *        (1 + edist_{z, R} f g) ^ (- τ ^ 2 / (2 + a)) := by      gcongr      · exact one_le_two      · linarith  /- Final step: control `‖∫ x, exp (I * (f x - g x)) * φ x‖ₑ` by adding up the estimates of the  two previous steps. -/  calc      ‖∫ x, exp (I * (f x - g x)) * φ x‖ₑ  _ = ‖∫ x, exp (I * (f x - g x)) * (φ x - φ' x) + exp (I * (f x - g x)) * φ' x‖ₑ := by    congr with x    ring  _ = ‖(∫ x, exp (I * (f x - g x)) * (φ x - φ' x)) + ∫ x, exp (I * (f x - g x)) * φ' x‖ₑ := by    rw [integral_add]    · apply Continuous.integrable_of_hasCompactSupport (by fun_prop)      exact (φ_comp.sub φ'_comp).mul_left    · apply Continuous.integrable_of_hasCompactSupport (by fun_prop)      exact φ'_comp.mul_left  _ ≤ ‖∫ x, exp (I * (f x - g x)) * (φ x - φ' x)‖ₑ + ‖∫ x, exp (I * (f x - g x)) * φ' x‖ₑ :=    enorm_add_le _ _  _ ≤ 2 ^ (6 * a) * volume (ball z R) * iHolENorm φ z (2 * R) τ *        (1 + edist_{z, R} f g) ^ (- τ ^ 2 / (2 + a)) +      2 ^ (6 * a) * volume (ball z R) * iHolENorm φ z (2 * R) τ *        (1 + edist_{z, R} f g) ^ (- τ ^ 2 / (2 + a)) := by gcongr;  _ = 2 ^ (1 + 6 * a) * volume (ball z R) * iHolENorm φ z (2 * R) τ *        (1 + edist_{z, R} f g) ^ (- τ ^ 2 / (2 + a)) := by rw [pow_add, pow_one]; ring  _ ≤ 2 ^ (7 * a) * volume (ball z R) * iHolENorm φ z (2 * R) τ *        (1 + edist_{z, R} f g) ^ (- τ ^ 2 / (2 + a)) := by    gcongr    · exact one_le_two    · linarith  _ = (C2_0_5 a : ℝ≥0∞) * volume (ball z R) * iHolENorm φ z (2 * R) τ *      (1 + edist_{z, R} f g) ^ (- (2 * a^2 + a^3 : ℝ)⁻¹) := by    congr    · simp only [C2_0_5]      rw [ENNReal.coe_rpow_of_nonneg]      · simp [← ENNReal.rpow_natCast]      · linarith    · simp [defaultτ]      field_simp