mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℝ
hb : 0 < b
⊢ 0 ≤ ∫ (x : ℝ), rexp (-b * x ^ 2)

Tactic:
by positivity

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℝ
hb : 0 < b
⊢ 0 ≤ √(π / b)

Tactic:
by positivity

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case zero
s : ℂ
h1 : 0 < s.re
⊢ s.GammaIntegral = s * s.GammaIntegral / s

Tactic:
mul_div_cancel_left₀

Goal state after:
case zero
s : ℂ
h1 : 0 < s.re
⊢ s.GammaIntegral = s.GammaIntegral

case zero.ha
s : ℂ
h1 : 0 < s.re
⊢ s ≠ 0
Module: Mathlib.Analysis.Fourier.Inversion

Goal state before:
pp: case e'_3
V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
hf : Integrable f volume
h'f : Integrable (𝓕 f) volume
v : V
this : Integrable (fun w ↦ 𝐞 ⟪w, v⟫ • 𝓕 f w) volume
c : ℝ
w : V
⊢ cexp (-↑c⁻¹ * ↑‖w‖ ^ 2 + 2 * ↑π * I * ↑⟪v, w⟫) • 𝓕 f w = cexp (-↑c⁻¹ * ↑‖w‖ ^ 2 + ↑(2 * π * ⟪w, v⟫) * I) • 𝓕 f w

Tactic:
real_inner_comm

Goal state after:
case e'_3
V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
hf : Integrable f volume
h'f : Integrable (𝓕 f) volume
v : V
this : Integrable (fun w ↦ 𝐞 ⟪w, v⟫ • 𝓕 f w) volume
c : ℝ
w : V
⊢ cexp (-↑c⁻¹ * ↑‖w‖ ^ 2 + 2 * ↑π * I * ↑⟪w, v⟫) • 𝓕 f w = cexp (-↑c⁻¹ * ↑‖w‖ ^ 2 + ↑(2 * π * ⟪w, v⟫) * I) • 𝓕 f w
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: a r : ℝ
ha : 0 < a
hr : 0 < r
⊢ 0 ≤ 1 / r

Tactic:
by positivity

Goal state after:
Module: Mathlib.Analysis.Fourier.Inversion

Goal state before:
pp: V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
hf : Integrable f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ := fun w ↦ π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)
x : V
⊢ 0 ≤ φ x

Tactic:
by positivity

Goal state after:
Module: Mathlib.Analysis.Fourier.Inversion

Goal state before:
pp: V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
hf : Integrable f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ := fun w ↦ π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)
⊢ 0 < π ^ 2

Tactic:
by positivity

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: k : ℕ
ih : Gamma (↑k + 1 + 1 / 2) = ↑(2 * k + 1)‼ * √π / 2 ^ (k + 1)
⊢ ↑(k + 1) + 1 / 2 ≠ 0

Tactic:
by positivity

Goal state after:
Module: Mathlib.Analysis.Fourier.Inversion

Goal state before:
pp: V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
hf : Integrable f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ := fun w ↦ π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)
A : Tendsto (fun w ↦ π ^ 2 * ‖w‖ ^ 2) (cobounded V) atTop
B :
  Tendsto
    (fun x ↦
      π ^ (-↑(finrank ℝ V) / 2) * ((fun x ↦ x ^ (↑(finrank ℝ V) / 2) * rexp (-1 * x)) ∘ fun w ↦ π ^ 2 * ‖w‖ ^ 2) x)
    (cobounded V) (𝓝 0)
x : V
⊢ 0 ≤ π ^ ↑2

Tactic:
by positivity

Goal state after:
Module: Mathlib.Analysis.Fourier.Inversion

Goal state before:
pp: V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
hf : Integrable f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ := fun w ↦ π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)
A : Tendsto (fun w ↦ π ^ 2 * ‖w‖ ^ 2) (cobounded V) atTop
B :
  Tendsto
    (fun x ↦
      π ^ (-↑(finrank ℝ V) / 2) * ((fun x ↦ x ^ (↑(finrank ℝ V) / 2) * rexp (-1 * x)) ∘ fun w ↦ π ^ 2 * ‖w‖ ^ 2) x)
    (cobounded V) (𝓝 0)
x : V
⊢ 0 ≤ ‖x‖ ^ ↑2

Tactic:
by positivity

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c : ℂ
this : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
⊢ 𝓕 (fun x ↦ cexp (-↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x)) t = 1 / b ^ (1 / 2) * cexp (-↑π / b * (↑t + I * c) ^ 2)

Tactic:
fourier_real_eq_integral_exp_smul,

Goal state after:
b : ℂ
hb : 0 < b.re
c : ℂ
this : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
⊢ ∫ (v : ℝ), cexp (↑(-2 * π * v * t) * I) • cexp (-↑π * b * ↑v ^ 2 + 2 * ↑π * c * ↑v) =
    1 / b ^ (1 / 2) * cexp (-↑π / b * (↑t + I * c) ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: case e_a
b : ℂ
hb : 0 < b.re
c : ℂ
this✝ : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    ↑(-2 * π * x * t) * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x =
      -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0
⊢ (b ^ (1 / 2))⁻¹ = 1 / b ^ (1 / 2)

pp: case e_a.hx
b : ℂ
hb : 0 < b.re
c : ℂ
this✝ : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    ↑(-2 * π * x * t) * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x =
      -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0
⊢ b.arg ≠ π

Tactic:
← one_div

Goal state after:
case e_a
b : ℂ
hb : 0 < b.re
c : ℂ
this✝ : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    ↑(-2 * π * x * t) * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x =
      -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0
⊢ 1 / b ^ (1 / 2) = 1 / b ^ (1 / 2)

case e_a.hx
b : ℂ
hb : 0 < b.re
c : ℂ
this✝ : b ≠ 0
h : (-↑π * b).re < 0
t : ℝ
this :
  ∀ (x : ℝ),
    ↑(-2 * π * x * t) * I + -↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x =
      -↑π * b * ↑x ^ 2 + (-2 * ↑π * I * ↑t + 2 * ↑π * c) * ↑x + 0
⊢ b.arg ≠ π
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c : ℂ
⊢ (𝓕 fun x ↦ cexp (-↑π * b * ↑x ^ 2 + 2 * ↑π * c * ↑x)) = fun t ↦ 1 / b ^ (1 / 2) * cexp (-↑π / b * (↑t + I * c) ^ 2)

Tactic:
have : b ≠ 0 := by contrapose! hb; rw [hb, zero_re]
  have h : (-↑π * b).re < 0 := by
    simpa only [neg_mul, neg_re, re_ofReal_mul, neg_lt_zero] using mul_pos pi_pos hb
  ext1 t
  simp_rw [fourier_real_eq_integral_exp_smul, smul_eq_mul, ← Complex.exp_add, ← add_assoc]
  have (x : ℝ) : ↑(-2 * π * x * t) * I + -π * b * x ^ 2 + 2 * π * c * x =
    -π * b * x ^ 2 + (-2 * π * I * t + 2 * π * c) * x + 0 := by push_cast; ring
  simp_rw [this, integral_cexp_quadratic h, neg_mul, neg_neg]
  congr 2
  · rw [← div_div, div_self <| ofReal_ne_zero.mpr pi_ne_zero, one_div, inv_cpow, ← one_div]
    rw [Ne, arg_eq_pi_iff, not_and_or, not_lt]
    exact Or.inl hb.le
  · field_simp
    ring_nf
    simp only [I_sq]
    ring

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
v : ι → ℝ
i : ι
_hi : i ∈ Finset.univ
⊢ 0 ≤ v i ^ 2

Tactic:
by positivity

Goal state after:
Module: Mathlib.Analysis.Fourier.Inversion

Goal state before:
pp: V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
hf : Integrable f volume
v : V
h'f : ContinuousAt f v
⊢ Tendsto (fun c ↦ ∫ (w : V), ((↑π * ↑c) ^ (↑(finrank ℝ V) / 2) * cexp (-↑π ^ 2 * ↑c * ↑‖v - w‖ ^ 2)) • f w) atTop
    (𝓝 (f v))

Tactic:
by
  let φ : V → ℝ := fun w ↦ π ^ (finrank ℝ V / 2 : ℝ) * Real.exp (-π ^ 2 * ‖w‖ ^ 2)
  have A : Tendsto (fun (c : ℝ) ↦ ∫ w : V, (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
      atTop (𝓝 (f v)) := by
    apply tendsto_integral_comp_smul_smul_of_integrable'
    · exact fun x ↦ by positivity
    · rw [integral_const_mul, GaussianFourier.integral_rexp_neg_mul_sq_norm (by positivity)]
      nth_rewrite 2 [← pow_one π]
      rw [← rpow_natCast, ← rpow_natCast, ← rpow_sub pi_pos, ← rpow_mul pi_nonneg,
        ← rpow_add pi_pos]
      ring_nf
      exact rpow_zero _
    · have A : Tendsto (fun (w : V) ↦ π ^ 2 * ‖w‖ ^ 2) (cobounded V) atTop := by
        rw [tendsto_const_mul_atTop_of_pos (by positivity)]
        apply (tendsto_pow_atTop two_ne_zero).comp tendsto_norm_cobounded_atTop
      have B := tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero (finrank ℝ V / 2) 1
        zero_lt_one |>.comp A |>.const_mul (π ^ (-finrank ℝ V / 2 : ℝ))
      rw [mul_zero] at B
      convert! B using 2 with x
      simp only [neg_mul, one_mul, Function.comp_apply, ← mul_assoc, ← rpow_natCast, φ]
      congr 1
      rw [mul_rpow (by positivity) (by positivity), ← rpow_mul pi_nonneg,
        ← rpow_mul (norm_nonneg _), ← mul_assoc, ← rpow_add pi_pos, mul_comm]
      congr <;> ring
    · exact hf
    · exact h'f
  have B : Tendsto
      (fun (c : ℝ) ↦
        ∫ w : V, ((c ^ (1 / 2 : ℝ)) ^ finrank ℝ V * φ ((c ^ (1 / 2 : ℝ)) • (v - w))) • f w)
      atTop (𝓝 (f v)) :=
    A.comp (tendsto_rpow_atTop (by simp))
  apply B.congr'
  filter_upwards [Ioi_mem_atTop 0] with c (hc : 0 < c)
  congr with w
  rw [← coe_smul]
  congr
  rw [ofReal_mul, ofReal_mul, ofReal_exp, ← mul_assoc]
  congr
  · rw [mul_cpow_ofReal_nonneg pi_nonneg hc.le, ← rpow_natCast, ← rpow_mul hc.le, mul_comm,
      ofReal_cpow pi_nonneg, ofReal_cpow hc.le]
    simp [div_eq_inv_mul]
  · norm_cast
    simp only [one_div, norm_smul, Real.norm_eq_abs, mul_pow, sq_abs, neg_mul, neg_inj,
      ← rpow_natCast, ← rpow_mul hc.le, mul_assoc]
    simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
y : ι → ℝ
i : ι
_hi : i ∈ Finset.univ
⊢ 0 ≤ y i ^ 2

Tactic:
by positivity

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
i : ι
_hi : i ∈ Finset.univ
⊢ 0 ≤ w.ofLp i ^ 2

Tactic:
by positivity

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
b : ℝ
hb : 0 < b
⊢ 0 ≤ π / b

Tactic:
by positivity

Goal state after:
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : RCLike 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
k n : ℕ
⊢ 0 ≤
    ((2 * π) ^ n * (2 * ↑n + 2) ^ k * ↑(Finset.range (n + 1) ×ˢ Finset.range (k + 1)).card *
          2 ^ volume.integrablePower *
        ∫ (x : V), (1 + ‖x‖) ^ (-↑volume.integrablePower)) *
      2

Tactic:
by positivity

Goal state after:
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier

Goal state before:
pp: E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_3
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : 𝓢(V, E)
⊢ ⇑(𝓕⁻ f) = 𝓕⁻ ⇑f

Tactic:
by
  ext x
  exact (fourierInv_eq_fourier_neg f x).symm

Goal state after:
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : RCLike 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : 𝓢(V, E)
x m : V
⊢ (𝓕 (fderiv ℝ ⇑f) x) m = (((2 * ↑π * Complex.I) • (smulRightCLM ℂ E (innerSL ℝ)) (𝓕 f)) x) m

Tactic:
simp [fourier_fderiv f.integrable f.differentiable (fderivCLM ℝ V E f).integrable,
    innerSL_apply_apply ℝ, fourier_coe]

Goal state after:
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier

Goal state before:
pp: V : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace ℝ V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : 𝓢(V, F)
⊢ 0 ≤ ‖f.toLp 1 volume‖

Tactic:
by positivity

Goal state after:
Module: Mathlib.Analysis.Distribution.Support

Goal state before:
pp: α : Type u_2
β : Type u_3
F : Type u_6
V : Type u_10
inst✝³ : FunLike F α β
inst✝² : TopologicalSpace α
inst✝¹ : Zero β
inst✝ : Zero V
f : F → V
⊢ (dsupport f)ᶜ = ⋃₀ {a | IsVanishingOn f a ∧ IsOpen[inst✝²] a}

Tactic:
simp [dsupport, Set.compl_sInter, Set.compl_image_ofPred]

Goal state after:
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : NormedSpace ℂ F
s s' : ℝ
f : 𝓢'(E, F)
x : E
⊢ 0 < 1 + ‖x‖ ^ 2

Tactic:
by positivity

Goal state after:
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: case h
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢(E, F)
⊢ (besselPotential E F s) ((SchwartzMap.toTemperedDistributionCLM E F volume) f) =
    Lp.toTemperedDistribution (((SchwartzMap.fourierMultiplierCLM F fun x ↦ (1 + ‖x‖ ^ 2) ^ (s / 2)) f).toLp p volume)

Tactic:
rw [besselPotential, Lp.toTemperedDistribution_toLp_eq,
    fourierMultiplierCLM_toTemperedDistributionCLM_eq (by fun_prop)]

Goal state after:
case h
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢(E, F)
⊢ (SchwartzMap.toTemperedDistributionCLM E F volume)
      ((SchwartzMap.fourierMultiplierCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) f) =
    (SchwartzMap.toTemperedDistributionCLM E F volume)
      ((SchwartzMap.fourierMultiplierCLM F fun x ↦ (1 + ‖x‖ ^ 2) ^ (s / 2)) f)
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
hs : ↑(Module.finrank ℝ E) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution u
h : ∫⁻ (a : E), ‖(1 + ‖a‖ ^ 2) ^ (-s)‖ₑ < ∞
x✝ : E
⊢ 0 ≤ 1 + ‖x✝‖ ^ 2

Tactic:
by positivity

Goal state after:
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
hs : ↑(Module.finrank ℝ E) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution u
x : E
⊢ 0 ≤ (1 + ‖x‖ ^ 2) ^ (-s)

Tactic:
by positivity

Goal state after:
Module: Mathlib.GroupTheory.FiniteAbelian.Basic

Goal state before:
pp: case zero
ι : Type
inst✝ : DecidableEq ι
p n : ι → ℕ
⊢ (directSumNeZeroMulHom p n)
      ((DirectSum.toAddMonoid fun i ↦ if h : n i = 0 then 0 else DirectSum.of (fun j ↦ ZMod (p ↑j ^ n ↑j)) ⟨i, h⟩) 0) =
    0

Tactic:
map_zero,

Goal state after:
case zero
ι : Type
inst✝ : DecidableEq ι
p n : ι → ℕ
⊢ (directSumNeZeroMulHom p n) 0 = 0
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
hs : ↑(Module.finrank ℝ E) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution u
this✝ : MemLp (fun x ↦ (1 + ‖x‖ ^ 2) ^ (-s / 2)) 2 volume
this : MemLp (fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (-s / 2))) 2 volume
x : E
⊢ 0 < 1 + ‖x‖ ^ 2

Tactic:
by positivity

Goal state after:
Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : Fintype α
ι : Type
w✝ : Fintype ι
n : ι → ℕ
hn : ∀ (i : ι), 1 < n i
e : α ≃+ ⨁ (i : ι), ZMod (n i)
i : ι
this : 1 < n i
⊢ n i ≠ 0

Tactic:
by positivity

Goal state after:
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s s' : ℝ
h : s' ≤ s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
h' : (s' - s) / 2 ≤ 0
hs : s' = s' - s + s
x : E
⊢ 0 ≤ (1 + ‖x‖ ^ 2) ^ ((s' - s) / 2)

Tactic:
by positivity

Goal state after:
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
m x : E
⊢ 0 ≤ ‖m‖

Tactic:
by positivity

Goal state after:
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
m x : E
⊢ 0 ≤ 1 + ‖x‖ ^ 2

Tactic:
by positivity

Goal state after:
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
x : E
⊢ 0 ≤ 1 + ‖x‖ ^ 2

Tactic:
by positivity

Goal state after:
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
x : E
⊢ 0 < (1 + ‖x‖ ^ 2) ^ 1

Tactic:
by positivity

Goal state after:
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: m n : ℕ+
⊢ (↑m).gcd ↑n = 1 ↔ m.gcd n = 1

Tactic:
rw [← coe_inj]

Goal state after:
m n : ℕ+
⊢ (↑m).gcd ↑n = 1 ↔ ↑(m.gcd n) = ↑1
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: case e'_3
f : C(ℝ, ℂ)
h_norm : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
h_sum : Summable fun n ↦ 𝓕 ⇑f ↑n
x : ℝ
F : C(UnitAddCircle, ℂ) := { toFun := ⋯.lift, continuous_toFun := ⋯ }
this : Summable (fourierCoeff ⇑F)
⊢ ∑' (n : ℤ), 𝓕 ⇑f ↑n * (fourier n) ↑x = ∑' (b : ℤ), fourierCoeff (⇑F) b • (fourier b) ↑x

Tactic:
simp_rw [← Real.fourierCoeff_tsum_comp_add h_norm, smul_eq_mul, F, coe_mk]

Goal state after:
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
⊢ y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)

Tactic:
obtain ⟨hx1, hx2⟩ := hx

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
⊢ y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case zero
⊢ (μ * ↑ζ) 0 = 1 0

Tactic:
map_zero,

Goal state after:
case zero
⊢ 0 = 1 0
Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Goal state before:
pp: E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
hf1 :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf2 : HasCompactSupport f
ε : ℝ
hε : ε > 0
R : ℝ
hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0
A : Set V := {v | ‖v‖ ≤ R + 1}
this : A = Metric.closedBall 0 (R + 1)
⊢ MeasurableSet A

Tactic:
rw [this]
      exact Metric.isClosed_closedBall.measurableSet

Goal state after:
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : c > 0
d : ℝ
hd : ∀ (b_1 : ℝ), d ≤ b_1 → ‖f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
⊢ 0 ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖

Tactic:
by positivity

Goal state after:
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : c > 0
d : ℝ
hd : ∀ (b_1 : ℝ), d ≤ b_1 → ‖f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x✝ : ℝ
hx : 1 + max 0 (-2 * R) ≤ x✝ ∧ d - R ≤ x✝
hx' : 0 < x✝ ∧ -2 * R < x✝
y : ↑(Icc (x✝ + R) (x✝ + S))
x : ℝ
⊢ 0 ≤ |x| ^ (-b)

Tactic:
by positivity

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
d n : ℕ
hdvd : d ∣ n
hn : n ≠ 0
⊢ 0 < n

Tactic:
by positivity

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
d n : ℕ
hdvd : d ∣ n
hn : n ≠ 0
h0d : 0 < d
⊢ 0 < n

Tactic:
by positivity

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : IsDomain R
hpos : 0 < n
μ : R
h : IsPrimitiveRoot μ n
⊢ μ ∈ primitiveRoots n R

Tactic:
rwa [← mem_primitiveRoots hpos] at h

Goal state after: