theorem abs_pow_sub_pow_le_mul (n : ℕ) {x y M : ℝ}
  (hx : 0 ≤ x) (hy : 0 ≤ y) (hxM : x ≤ M)
  (hyM : y ≤ M) :
  |x ^ n - y ^ n| ≤
    ↑n * M ^ (n - 1) * |x - y|

theorem norm_sub_taylorSum_le.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  {f : ℝ → E} {k : ℕ} {C a h : ℝ}
  (hf : ContDiff ℝ (↑(k + 1)) f)
  (hC :
    ∀ y ∈ Set.uIcc a (a + h),
      ‖iteratedDeriv (k + 1) f y‖ ≤ C) :
  ‖f (a + h) -
        ∑ j ∈ Finset.range (k + 1),
          (h ^ j / ↑j.factorial) •
            iteratedDeriv j f a‖ ≤
    C * |h| ^ (k + 1) / ↑k.factorial

theorem MeasureTheory.tendsto_setIntegral_norm_abs_gt.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  {g : ℝ → E}
  (hg :
    MeasureTheory.Integrable g
      MeasureTheory.volume) :
  Filter.Tendsto
    (fun c ↦
      ∫ (r : ℝ) in {r | c < |r|}, ‖g r‖)
    Filter.atTop (nhds 0)

theorem MeasureTheory.tendsto_integral_norm_sub_comp_sub_right.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  {Ξ : ℝ → E}
  (hΞ :
    MeasureTheory.Integrable Ξ
      MeasureTheory.volume) :
  Filter.Tendsto
    (fun s ↦ ∫ (z : ℝ), ‖Ξ (z - s) - Ξ z‖)
    (nhds 0) (nhds 0)

theorem MeasureTheory.tendsto_integral_weight_norm_sub_comp_sub_right.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  (k : ℕ) {Ξ : ℝ → E} [NormedSpace ℝ E]
  (hΞm :
    MeasureTheory.AEStronglyMeasurable Ξ
      MeasureTheory.volume)
  (hΞk :
    MeasureTheory.Integrable
      (fun r ↦ (1 + |r|) ^ k * ‖Ξ r‖)
      MeasureTheory.volume) :
  Filter.Tendsto
    (fun s ↦
      ∫ (z : ℝ),
        (1 + |z|) ^ k * ‖Ξ (z - s) - Ξ z‖)
    (nhds 0) (nhds 0)

theorem MeasureTheory.integrable_weight_norm_comp_sub.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  (k : ℕ) {Ξ : ℝ → E}
  (hΞm :
    MeasureTheory.AEStronglyMeasurable Ξ
      MeasureTheory.volume)
  (hΞk :
    MeasureTheory.Integrable
      (fun r ↦ (1 + |r|) ^ k * ‖Ξ r‖)
      MeasureTheory.volume)
  (s : ℝ) :
  MeasureTheory.Integrable
    (fun z ↦ (1 + |z|) ^ k * ‖Ξ (z - s)‖)
    MeasureTheory.volume

theorem MeasureTheory.integrable_weight_norm_sub_comp_sub.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  (k : ℕ) {Ξ : ℝ → E}
  (hΞm :
    MeasureTheory.AEStronglyMeasurable Ξ
      MeasureTheory.volume)
  (hΞk :
    MeasureTheory.Integrable
      (fun r ↦ (1 + |r|) ^ k * ‖Ξ r‖)
      MeasureTheory.volume)
  (s : ℝ) :
  MeasureTheory.Integrable
    (fun z ↦
      (1 + |z|) ^ k * ‖Ξ (z - s) - Ξ z‖)
    MeasureTheory.volume

theorem MeasureTheory.continuous_integral_weight_norm_sub.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  (k : ℕ) [NormedSpace ℝ E] {Ξ : ℝ → E}
  (hΞm :
    MeasureTheory.AEStronglyMeasurable Ξ
      MeasureTheory.volume)
  (hΞk :
    MeasureTheory.Integrable
      (fun r ↦ (1 + |r|) ^ k * ‖Ξ r‖)
      MeasureTheory.volume) :
  Continuous fun s ↦
    ∫ (z : ℝ),
      (1 + |z|) ^ k * ‖Ξ (z - s) - Ξ z‖

theorem MeasureTheory.integral_comp_sub_div_smul.{u_2}
  {E : Type u_2} [NormedAddCommGroup E]
  [NormedSpace ℝ E] (F : ℝ → E) (r : ℝ)
  {c : ℝ} (hc : 0 < c) :
  ∫ (w : ℝ), F ((w - r) / c) =
    c • ∫ (v : ℝ), F v

theorem MeasureTheory.tendsto_integral_weight_norm_smoothing_sub
  (k : ℕ) {Ξ K : ℝ → ℂ}
  (hΞm :
    MeasureTheory.StronglyMeasurable Ξ)
  (hΞk :
    MeasureTheory.Integrable
      (fun r ↦ (1 + |r|) ^ k * ‖Ξ r‖)
      MeasureTheory.volume)
  (hKm :
    MeasureTheory.AEStronglyMeasurable K
      MeasureTheory.volume)
  (hKk :
    MeasureTheory.Integrable
      (fun u ↦ (1 + |u|) ^ k * ‖K u‖)
      MeasureTheory.volume)
  (hK1 : ∫ (u : ℝ), K u = 1) :
  Filter.Tendsto
    (fun c ↦
      ∫ (z : ℝ),
        (1 + |z|) ^ k *
          ‖(∫ (u : ℝ),
                K u * Ξ (z - u / c)) -
              Ξ z‖)
    Filter.atTop (nhds 0)

theorem MeasureTheory.tendsto_integral_mul_smoothing_of_vanishing_moments
  (k : ℕ) {η Ξ : ℝ → ℂ} {Cη : ℝ}
  (θ : SchwartzMap ℝ ℂ)
  (hηm :
    MeasureTheory.StronglyMeasurable η)
  (hηk :
    ∀ (z : ℝ), ‖η z‖ ≤ Cη * (1 + |z|) ^ k)
  (hΞm :
    MeasureTheory.AEStronglyMeasurable Ξ
      MeasureTheory.volume)
  (hΞk :
    MeasureTheory.Integrable
      (fun r ↦ (1 + |r|) ^ k * ‖Ξ r‖)
      MeasureTheory.volume)
  (hΞvm :
    ∀ j ≤ k,
      ∫ (r : ℝ), ↑r ^ j * Ξ r = 0) :
  Filter.Tendsto
    (fun c ↦
      ∫ (r : ℝ),
        Ξ r *
          (↑c⁻¹ *
            ∫ (w : ℝ),
              η w * θ ((w - r) / c)))
    Filter.atTop (nhds 0)

theorem mem_lizorkinSpace_iff
  {φ : SchwartzMap ℝ ℂ} :
  φ ∈ LizorkinSpace ↔
    ∀ (n : ℕ), ∫ (z : ℝ), ↑z ^ n * φ z = 0

theorem integrable_pow_smul_schwartz
  (φ : SchwartzMap ℝ ℂ) (n : ℕ) :
  MeasureTheory.Integrable
    (fun z ↦ ↑z ^ n * φ z)
    MeasureTheory.volume

theorem Real.fourier_apply_zero (g : ℝ → ℂ) :
  FourierTransform.fourier g 0 =
    ∫ (z : ℝ), g z

theorem Real.iteratedDeriv_fourier_zero
  (φ : SchwartzMap ℝ ℂ) (n : ℕ) :
  iteratedDeriv n
      (FourierTransform.fourier ⇑φ) 0 =
    (-2 * ↑Real.pi * Complex.I) ^ n *
      ∫ (z : ℝ), ↑z ^ n * φ z

theorem mem_lizorkinSpace_iff_fourier_flat
  {φ : SchwartzMap ℝ ℂ} :
  φ ∈ LizorkinSpace ↔
    ∀ (n : ℕ),
      iteratedDeriv n
          (FourierTransform.fourier ⇑φ)
          0 =
        0

theorem integral_polynomial_mul_eq_zero_of_mem_lizorkinSpace
  {φ : SchwartzMap ℝ ℂ}
  (hφ : φ ∈ LizorkinSpace)
  (Q : Polynomial ℂ) :
  ∫ (z : ℝ),
      Polynomial.eval (↑z) Q * φ z =
    0

theorem MeasureTheory.polynomiallyBounded_nonneg_const
  {η : ℝ → ℂ} {C : ℝ} {k : ℕ}
  (h :
    ∀ (z : ℝ),
      ‖η z‖ ≤ C * (1 + |z|) ^ k) :
  0 ≤ C

theorem MeasureTheory.PolynomiallyBounded.add
  {η₁ η₂ : ℝ → ℂ}
  (h₁ :
    MeasureTheory.PolynomiallyBounded η₁)
  (h₂ :
    MeasureTheory.PolynomiallyBounded
      η₂) :
  MeasureTheory.PolynomiallyBounded
    fun z ↦ η₁ z + η₂ z

theorem MeasureTheory.polynomiallyBounded_polynomial_eval
  (Q : Polynomial ℂ) :
  MeasureTheory.PolynomiallyBounded
    fun z ↦ Polynomial.eval (↑z) Q

theorem MeasureTheory.PolynomiallyBounded.integrable_mul_schwartz
  {η : ℝ → ℂ}
  (hb :
    MeasureTheory.PolynomiallyBounded η)
  (hm :
    MeasureTheory.AEStronglyMeasurable η
      MeasureTheory.volume)
  (φ : SchwartzMap ℝ ℂ) :
  MeasureTheory.Integrable
    (fun z ↦ η z * φ z)
    MeasureTheory.volume

theorem one_add_abs_add_le_mul (z t : ℝ) :
  1 + |z + t| ≤ (1 + |z|) * (1 + |t|)

theorem MeasureTheory.integrable_one_add_abs_pow_mul_schwartz
  (φ : SchwartzMap ℝ ℂ) (k : ℕ) :
  MeasureTheory.Integrable
    (fun s ↦ (1 + |s|) ^ k * ‖φ s‖)
    MeasureTheory.volume

theorem MeasureTheory.integral_pow_mul_conj_comp_sub_eq_zero
  {ψ : ℝ → ℂ} {k : ℕ}
  (hψm :
    MeasureTheory.AEStronglyMeasurable ψ
      MeasureTheory.volume)
  (hψk :
    MeasureTheory.Integrable
      (fun s ↦ (1 + |s|) ^ k * ‖ψ s‖)
      MeasureTheory.volume)
  (hψvm :
    ∀ j ≤ k, ∫ (s : ℝ), ↑s ^ j * ψ s = 0)
  {j : ℕ} (hj : j ≤ k) (c : ℝ) :
  ∫ (r : ℝ),
      ↑r ^ j *
        (starRingEnd ℂ) (ψ (r - c)) =
    0

theorem coe_iterate_schwartz_derivCLM (n : ℕ)
  (φ : SchwartzMap ℝ ℂ) :
  ⇑((⇑(SchwartzMap.derivCLM ℂ ℂ))^[n] φ) =
    iteratedDeriv n ⇑φ

theorem iteratedDeriv_eq_zero_of_tsupport_subset_compl
  (φ : SchwartzMap ℝ ℂ)
  (hφ : tsupport ⇑φ ⊆ {0}ᶜ) (n : ℕ) :
  iteratedDeriv n (⇑φ) 0 = 0

theorem exists_pos_le_abs_of_tsupport_subset
  {g : ℝ → ℂ} (hg : tsupport g ⊆ {0}ᶜ) :
  ∃ δ > 0, ∀ ζ ∈ tsupport g, δ ≤ |ζ|

theorem MeasureTheory.integrable_mul_of_bound_on_tsupport
  {c g : ℝ → ℂ} {C : ℝ}
  (hc :
    MeasureTheory.AEStronglyMeasurable c
      MeasureTheory.volume)
  (hg :
    MeasureTheory.Integrable g
      MeasureTheory.volume)
  (hbound : ∀ ζ ∈ tsupport g, ‖c ζ‖ ≤ C) :
  MeasureTheory.Integrable
    (fun ζ ↦ c ζ * g ζ)
    MeasureTheory.volume

theorem hasTemperateGrowth_const_mul (c : ℝ) :
  Function.HasTemperateGrowth fun ζ ↦
    c * ζ

theorem antilipschitzWith_const_mul {c : ℝ}
  (hc : c ≠ 0) :
  AntilipschitzWith (Real.nnabs c⁻¹)
    fun ζ ↦ c * ζ

theorem MeasureTheory.enorm_integral_mul_sub_le.{u_1}
  {G : Type u_1} [MeasurableSpace G]
  [Sub G] {μ : MeasureTheory.Measure G}
  (f g : G → ℂ) (x : G) :
  ‖∫ (t : G), f t * g (x - t) ∂μ‖ₑ ≤
    ∫⁻ (t : G), ‖f t‖ₑ * ‖g (x - t)‖ₑ ∂μ

theorem MeasureTheory.lintegral_lintegral_mul_comp_sub.{u_1}
  {G : Type u_1} [MeasurableSpace G]
  [AddCommGroup G] [MeasurableAdd₂ G]
  [MeasurableNeg G]
  {μ : MeasureTheory.Measure G}
  [MeasureTheory.SFinite μ]
  [μ.IsAddRightInvariant]
  (F K : G → ENNReal)
  (hF : AEMeasurable F μ)
  (hK : AEMeasurable K μ) :
  ∫⁻ (x : G),
      ∫⁻ (t : G), F t * K (x - t) ∂μ ∂μ =
    (∫⁻ (t : G), F t ∂μ) *
      ∫⁻ (y : G), K y ∂μ

theorem MeasureTheory.eLpNorm_convolution_le.{u_1}
  {G : Type u_1} [MeasurableSpace G]
  [AddCommGroup G] [MeasurableAdd₂ G]
  [MeasurableNeg G]
  {μ : MeasureTheory.Measure G}
  [MeasureTheory.SFinite μ]
  [μ.IsAddLeftInvariant]
  [μ.IsAddRightInvariant]
  [μ.IsNegInvariant] {p : ENNReal}
  (hp : 1 ≤ p) {f g : G → ℂ}
  (hf :
    MeasureTheory.AEStronglyMeasurable f
      μ)
  (hg :
    MeasureTheory.AEStronglyMeasurable g
      μ) :
  MeasureTheory.eLpNorm
      (fun x ↦
        ∫ (t : G), f t * g (x - t) ∂μ)
      p μ ≤
    MeasureTheory.eLpNorm f 1 μ *
      MeasureTheory.eLpNorm g p μ