mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
v : V
n : ℕ
⊢ ‖fourierPowSMulRight L f v n‖ ≤ (2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖

Tactic:
apply ContinuousMultilinearMap.opNorm_le_bound (by positivity) (fun m ↦ ?_)

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
v : V
n : ℕ
m : Fin n → W
⊢ ‖(fourierPowSMulRight L f v n) m‖ ≤ (2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖ * ∏ i, ‖m i‖
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
K : ℕ∞ω
C : ℝ
hf : ContDiff ℝ K f
n k : ℕ
hk : ↑k ≤ K
v : V
hv : ∀ i ≤ k, ∀ j ≤ n, ‖v‖ ^ j * ‖iteratedFDeriv ℝ i f v‖ ≤ C
T : (W →L[ℝ] ℝ) [×n]→L[ℝ] W [×n]→L[ℝ] ℝ :=
  (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight
m : ℕ
this : ‖T‖ ≤ 1
⊢ 0 ≤ ‖L‖ * ‖v‖

Tactic:
by positivity

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAlgebra ℝ 𝕜
inst✝⁴ : NormedAddCommGroup D
inst✝³ : NormedSpace ℝ D
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
inst✝ : NormedSpace 𝕜 F
L : E →L[ℝ] G →L[ℝ] ℝ
k n : ℕ
⊢ 0 ≤ 2 * ‖L‖ * ↑(max 1 n)

Tactic:
by positivity

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup D
inst✝¹ : NormedSpace ℝ D
inst✝ : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N g x‖ ≤ C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : 0 ≤ Cg * (1 + ‖g 0‖) ^ kg
⊢ 0 < (1 + ‖g 0‖) ^ kg

Tactic:
by positivity

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup D
inst✝¹ : NormedSpace ℝ D
inst✝ : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N g x‖ ≤ C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
hCg : 1 ≤ 1 + Cg
k' : ℕ := kg * (k + l * n)
⊢ 0 ≤ (1 + Cg) ^ (k + l * n) * ((C + 1) ^ n * ↑n ! * 2 ^ k')

Tactic:
by positivity

Goal state after:
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
c : ℝ
hc : 0 ≤ c
x : F
⊢ 0 ≤ c ^ finrank ℝ F

Tactic:
by positivity

Goal state after:
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
⊢ δ ^ finrank ℝ F * ε > 0

Tactic:
by positivity

Goal state after:
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, x ∈ (closedBall 0 M)ᶜ → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
hc : M / δ < c
x : F
hx : x ∈ uᶜ
⊢ 0 < M / δ

Tactic:
by positivity

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup D
inst✝¹ : NormedSpace ℝ D
inst✝ : NormedSpace 𝕜 F
K : ℝ≥0
g : D → E
hg : Function.HasTemperateGrowth g
h'g : AntilipschitzWith K g
x : D
⊢ 0 ≤ ↑K

Tactic:
by positivity

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace ℝ G
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace ℝ H
inst✝ : NormedSpace 𝕜 H
L : F →L[𝕜] G
k n : ℕ
⊢ 0 ≤ ‖L‖

Tactic:
by positivity

Goal state after:
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, x ∈ (closedBall 0 M)ᶜ → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
hc : M / δ < c
x : F
hx : x ∈ uᶜ
cpos : 0 < c
hδx : δ ≤ ‖x‖
this : δ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x)) < δ ^ finrank ℝ F * ε
⊢ 0 < δ ^ finrank ℝ F

Tactic:
by positivity

Goal state after:
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, x ∈ (closedBall 0 M)ᶜ → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
hc : M / δ < c
x : F
hx : x ∈ uᶜ
cpos : 0 < c
hδx : δ ≤ ‖x‖
⊢ 0 ≤ c ^ finrank ℝ F

Tactic:
by positivity

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace ℝ D
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedSpace ℝ V
inst✝³ : NormedSpace 𝕜 V
inst✝² : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
inst✝¹ : BorelSpace D
inst✝ : SecondCountableTopology D
n : ℕ
h : Integrable (fun x ↦ (1 + ‖x‖) ^ (-↑n)) μ
m : ℕ × ℕ := (n, 0)
⊢ 0 ≤ 2 ^ n * ∫ (x : D), (1 + ‖x‖) ^ (-↑n) ∂μ

Tactic:
by positivity

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace ℝ D
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedSpace ℝ V
inst✝³ : NormedSpace 𝕜 V
inst✝² : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
inst✝¹ : BorelSpace D
inst✝ : SecondCountableTopology D
n : ℕ
h : Integrable (fun x ↦ (1 + ‖x‖) ^ (-↑n)) μ
m : ℕ × ℕ := (n, 0)
f : 𝓢(D, V)
x : D
⊢ 0 ≤ 1 + ‖x‖

Tactic:
by positivity

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace ℝ D
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedSpace ℝ V
inst✝³ : NormedSpace 𝕜 V
inst✝² : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
inst✝¹ : BorelSpace D
inst✝ : SecondCountableTopology D
n : ℕ
h : Integrable (fun x ↦ (1 + ‖x‖) ^ (-↑n)) μ
m : ℕ × ℕ := (n, 0)
f : 𝓢(D, V)
x : D
⊢ 0 < (1 + ‖x‖) ^ ↑n

Tactic:
by positivity

Goal state after:
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, x ∈ (closedBall 0 M)ᶜ → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
hc : M / δ < c
x : F
hx : x ∈ uᶜ
cpos : 0 < c
hδx : δ ≤ ‖x‖
⊢ ‖c • x‖ ^ finrank ℝ F * φ (c • x) < δ ^ finrank ℝ F * ε

Tactic:
apply hM

Goal state after:
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, x ∈ (closedBall 0 M)ᶜ → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
hc : M / δ < c
x : F
hx : x ∈ uᶜ
cpos : 0 < c
hδx : δ ≤ ‖x‖
⊢ c • x ∈ (closedBall 0 M)ᶜ
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, x ∈ (closedBall 0 M)ᶜ → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
hc : M / δ < c
x : F
hx : x ∈ uᶜ
cpos : 0 < c
hδx : δ ≤ ‖x‖
⊢ c • x ∈ (closedBall 0 M)ᶜ

Tactic:
div_lt_iff₀ δpos

Goal state after:
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, x ∈ (closedBall 0 M)ᶜ → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
hc : M < c * δ
x : F
hx : x ∈ uᶜ
cpos : 0 < c
hδx : δ ≤ ‖x‖
⊢ c • x ∈ (closedBall 0 M)ᶜ
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
w : W
⊢ fourierPowSMulRight (-L.flip) (iteratedFDeriv ℝ k (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f)) w n =
    fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (iteratedFDeriv ℝ n fun v ↦ fourierPowSMulRight L f v k) w

Tactic:
fourierIntegral_iteratedFDeriv (N := N) _ (hf.fourierPowSMulRight _ _) _ hn

Goal state after:
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
w : W
⊢ fourierPowSMulRight (-L.flip) (iteratedFDeriv ℝ k (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f)) w n =
    (fun w ↦
        fourierPowSMulRight (-L.flip)
          (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) fun v ↦ fourierPowSMulRight L f v k) w n)
      w

E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
w : W
⊢ ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedFDeriv ℝ n fun v ↦ fourierPowSMulRight L f v k) μ
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
⊢ 0 ≤ (SchwartzMap.seminorm ℝ 0 0) f

Tactic:
by positivity

Goal state after:
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
this : Tendsto (fun c ↦ ∫ (x : F) in closedBall 0 c, φ x ∂μ) atTop (𝓝 1)
c : ℝ
hc : 0 < c
⊢ c ^ finrank ℝ F ≠ 0

Tactic:
by positivity

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

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : SecondCountableTopologyEither E F
f : 𝓢(E, F)
p : ℝ≥0∞
μ : Measure E
hp₁ : p ≠ 0
hp₂ : p ≠ ∞
hμ : μ.HasTemperateGrowth
⊢ 0 ≤ (∫ (a : E), ‖f a‖ ^ p.toReal ∂μ) ^ p.toReal⁻¹

Tactic:
by positivity

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

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : SecondCountableTopologyEither E F
f : 𝓢(E, F)
μ : Measure E
hμ : μ.HasTemperateGrowth
⊢ 0 ≤ (SchwartzMap.seminorm ℝ 0 0) f

Tactic:
by positivity

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

Goal state before:
pp: H : Type u_8
V : Type u_9
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : NormedSpace ℝ H
inst✝⁵ : FiniteDimensional ℝ H
inst✝⁴ : MeasurableSpace H
inst✝³ : BorelSpace H
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℂ V
f g : 𝓢(H, V)
μ : Measure H
inst✝ : μ.HasTemperateGrowth
hf_ae : ↑↑(f.toLp 2 μ) =ᵐ[μ] ⇑f
hg_ae : ↑↑(g.toLp 2 μ) =ᵐ[μ] ⇑g
a✝ : H
hf : ↑↑(f.toLp 2 μ) a✝ = f a✝
hg : ↑↑(g.toLp 2 μ) a✝ = g a✝
⊢ inner ℂ (↑↑(f.toLp 2 μ) a✝) (↑↑(g.toLp 2 μ) a✝) = inner ℂ (f a✝) (g a✝)

Tactic:
hf,

Goal state after:
H : Type u_8
V : Type u_9
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : NormedSpace ℝ H
inst✝⁵ : FiniteDimensional ℝ H
inst✝⁴ : MeasurableSpace H
inst✝³ : BorelSpace H
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℂ V
f g : 𝓢(H, V)
μ : Measure H
inst✝ : μ.HasTemperateGrowth
hf_ae : ↑↑(f.toLp 2 μ) =ᵐ[μ] ⇑f
hg_ae : ↑↑(g.toLp 2 μ) =ᵐ[μ] ⇑g
a✝ : H
hf : ↑↑(f.toLp 2 μ) a✝ = f a✝
hg : ↑↑(g.toLp 2 μ) a✝ = g a✝
⊢ inner ℂ (f a✝) (↑↑(g.toLp 2 μ) a✝) = inner ℂ (f a✝) (g a✝)
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: 𝕜 : Type u_1
inst✝²³ : CommRing 𝕜
V : Type u_2
inst✝²² : AddCommGroup V
inst✝²¹ : Module 𝕜 V
inst✝²⁰ : MeasurableSpace V
W : Type u_3
inst✝¹⁹ : AddCommGroup W
inst✝¹⁸ : Module 𝕜 W
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℂ E
inst✝¹⁵ : NormedAddCommGroup F
inst✝¹⁴ : NormedSpace ℂ F
inst✝¹³ : NormedAddCommGroup G
inst✝¹² : NormedSpace ℂ G
inst✝¹¹ : TopologicalSpace 𝕜
inst✝¹⁰ : IsTopologicalRing 𝕜
inst✝⁹ : TopologicalSpace V
inst✝⁸ : BorelSpace V
inst✝⁷ : TopologicalSpace W
inst✝⁶ : MeasurableSpace W
inst✝⁵ : BorelSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
ν : Measure W
inst✝⁴ : SigmaFinite μ
inst✝³ : SigmaFinite ν
inst✝² : SecondCountableTopologyEither W V
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
f : V → E
g : W → F
M : E →L⋆[ℂ] F →L[ℂ] G
he : Continuous[inst✝¹¹, _] ⇑e
hL : Continuous[instTopologicalSpaceProd, inst✝¹¹] fun p ↦ (L p.1) p.2
hf : Integrable f μ
hg : Integrable g ν
⊢ ∫ (ξ : W), (M (fourierIntegral e μ L f ξ)) (g ξ) ∂ν = ∫ (x : V), (M (f x)) (fourierIntegral e ν (-L.flip) g x) ∂μ

Tactic:
by
  by_cases hG : CompleteSpace G; swap; · simp [integral, hG]
  calc
  ∫ ξ, M.flip (g ξ) (∫ x, e (-L x ξ) • f x ∂μ) ∂ν
    = ∫ ξ, (∫ x, M.flip (g ξ) (e (-L x ξ) • f x) ∂μ) ∂ν := by
    congr with ξ
    apply (ContinuousLinearMap.integral_comp_commSL RCLike.conj_smul _ _).symm
    exact (fourierIntegral_convergent_iff he hL _).2 hf
  _ = ∫ x, (∫ ξ, M.flip (g ξ) (e (-L x ξ) • f x) ∂ν) ∂μ :=
    integral_fourierIntegral_swap M.flip he hL hf hg
  _ = ∫ x, (∫ ξ, M (f x) (e (L.flip ξ x) • g ξ) ∂ν) ∂μ := by
    congr with x
    congr with ξ
    rw [← smul_one_smul ℂ _ (f x), ← smul_one_smul ℂ _ (g ξ)]
    simp only [map_smulₛₗ, ContinuousLinearMap.flip_apply, LinearMap.flip_apply, RingHom.id_apply,
      Circle.smul_def, smul_eq_mul, mul_one, ← Circle.coe_inv_eq_conj, AddChar.map_neg_eq_inv,
      inv_inv]
  _ = ∫ x, (∫ ξ, M (f x) (e (-(-L.flip ξ) x) • g ξ) ∂ν) ∂μ := by
    simp only [LinearMap.flip_apply, ContinuousLinearMap.map_smul_of_tower, LinearMap.neg_apply,
      neg_neg]
  _ = ∫ x, M (f x) (∫ ξ, e (-(-L.flip ξ) x) • g ξ ∂ν) ∂μ := by
    congr with x
    apply ContinuousLinearMap.integral_comp_comm
    have hLflip : Continuous fun (p : W × V) => (-L.flip p.1) p.2 :=
      (continuous_neg.comp hL).comp continuous_swap
    exact (fourierIntegral_convergent_iff (L := -L.flip) he hLflip x).2 hg

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

Goal state before:
pp: E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
v : V
w : W
⊢ 0 ≤ |(L v) w| ^ n * ‖iteratedFDeriv ℝ k (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f) w‖

Tactic:
by positivity

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

Goal state before:
pp: V : Type u_1
W : Type u_2
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : InnerProductSpace ℝ V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : InnerProductSpace ℝ W
inst✝³ : MeasurableSpace W
inst✝² : BorelSpace W
inst✝¹ : FiniteDimensional ℝ W
inst✝ : FiniteDimensional ℝ V
f : ↥(Lp E 1 volume)
⊢ 0 ≤ ‖f‖

Tactic:
by positivity

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

Goal state before:
pp: s : ℝ
this : ∀ (r : ℝ), ↑r = ↑r
⊢ (↑s).GammaIntegral = ↑(∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1))

Tactic:
rw [GammaIntegral]

Goal state after:
s : ℝ
this : ∀ (r : ℝ), ↑r = ↑r
⊢ ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (↑s - 1) = ↑(∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1))