mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Group.ZeroAtInfty

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝² : SeminormedAddGroup E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), 0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
s : Set ℝ
hs : s ∈ 𝓝 0
⊢ ∃ r, (Metric.closedBall 0 r)ᶜ ⊆ (fun x ↦ ‖f x‖) ⁻¹' s

Tactic:
Metric.mem_nhds_iff

Goal state after:
E : Type u_1
F : Type u_2
inst✝² : SeminormedAddGroup E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), 0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
s : Set ℝ
hs : ∃ ε > 0, Metric.ball 0 ε ⊆ s
⊢ ∃ r, (Metric.closedBall 0 r)ᶜ ⊆ (fun x ↦ ‖f x‖) ⁻¹' s
Module: Mathlib.Analysis.Normed.Group.ZeroAtInfty

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝² : SeminormedAddGroup E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), 0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
⊢ Tendsto f (cocompact E) (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
x : E
c : 𝕜
hc : c ≠ 0
⊢ T.rayleighQuotient (c • x) = T.rayleighQuotient x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T S : E →L[𝕜] E
x : E
⊢ (T + S).rayleighQuotient x = T.rayleighQuotient x + S.rayleighQuotient x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ rayleighQuotient 0 x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
⊢ T.rayleighQuotient 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
x : E
⊢ (-T).rayleighQuotient x = -T.rayleighQuotient x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
x : E
⊢ T.rayleighQuotient (-x) = T.rayleighQuotient x

Tactic:
by

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

Goal state before:
pp: H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y | 1 / 2 < y}
ht : (Set.range fun x ↦ 1 + ‖x‖ ^ 2) ⊆ t
hdiff : ContDiffOn ℝ ∞ (fun x ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r ((↑N - r) * Real.log 2 / Real.log (3 / 2)) ≤ ↑k
hk₁ : r ≤ ↑k
⊢ Real.log 2 * (↑N - r) ≤ Real.log (3 / 2) * ↑k

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedSpace 𝕜 F
n k : ℕ∞
inst✝¹ : Algebra ℝ 𝕜
inst✝ : IsScalarTower ℝ 𝕜 F
f : 𝓓^{n}(Ω, F)
v x : E
⊢ ((lineDerivCLM 𝕜 v) f) x = if k + 1 ≤ n then lineDeriv ℝ (⇑f) x v else 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
a : ℝ
x : E
hx : x ≠ 0
hxT : T.rayleighQuotient x = a
c : 𝕜 := ↑‖x‖⁻¹ * ↑r
⊢ c ≠ 0

Tactic:
by

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

Goal state before:
pp: H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y | 1 / 2 < y}
ht : (Set.range fun x ↦ 1 + ‖x‖ ^ 2) ⊆ t
hdiff : ContDiffOn ℝ ∞ (fun x ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r ((↑N - r) * Real.log 2 / Real.log (3 / 2)) ≤ ↑k
hk₁ : r ≤ ↑k
hk₂ : Real.log 2 * (↑N - r) ≤ Real.log (3 / 2) * ↑k
⊢ 0 ≤ ∑ k ∈ Finset.range (N + 1), ‖Polynomial.eval r (descPochhammer ℝ k)‖

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedSpace 𝕜 F
n k : ℕ∞
inst✝¹ : Algebra ℝ 𝕜
inst✝ : IsScalarTower ℝ 𝕜 F
f : 𝓓^{n}(Ω, F)
v x : E
hk : k + 1 ≤ n
⊢ ((lineDerivCLM 𝕜 v) f) x = lineDeriv ℝ (⇑f) x v

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedSpace 𝕜 F
n k : ℕ∞
inst✝¹ : Algebra ℝ 𝕜
inst✝ : IsScalarTower ℝ 𝕜 F
v : E
hk : n < k + 1
⊢ lineDerivCLM 𝕜 v = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
⊢ T.rayleighQuotient '' {0}ᶜ = T.rayleighQuotient '' sphere 0 r

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedSpace 𝕜 F
n k : ℕ∞
inst✝¹ : Algebra ℝ 𝕜
inst✝ : IsScalarTower ℝ 𝕜 F
v₁ v₂ : E
⊢ lineDerivCLM 𝕜 (v₁ + v₂) = lineDerivCLM 𝕜 v₁ + lineDerivCLM 𝕜 v₂

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedSpace 𝕜 F
n k : ℕ∞
inst✝¹ : Algebra ℝ 𝕜
inst✝ : IsScalarTower ℝ 𝕜 F
c : ℝ
v : E
⊢ lineDerivCLM 𝕜 (c • v) = c • lineDerivCLM 𝕜 v

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
x : E
⊢ |T.rayleighQuotient x| ≤ ‖T‖

Tactic:
by

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

Goal state before:
pp: H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y | 1 / 2 < y}
ht : (Set.range fun x ↦ 1 + ‖x‖ ^ 2) ⊆ t
hdiff : ContDiffOn ℝ ∞ (fun x ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r ((↑N - r) * Real.log 2 / Real.log (3 / 2)) ≤ ↑k
hk₁ : r ≤ ↑k
hk₂ : Real.log 2 * (↑N - r) ≤ Real.log (3 / 2) * ↑k
n : ℕ
hn : n ≤ N
x : ℝ
hx : x ∈ t
⊢ 0 < 1 / 2

Tactic:
by

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

Goal state before:
pp: E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
n : ℕ∞
m : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
f : 𝓓^{n}(Ω, F)
⊢ StronglyMeasurable ⇑f

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
m : MeasurableSpace E
inst✝⁷ : OpensMeasurableSpace E
F₁ : Type u_6
F₂ : Type u_7
F₃ : Type u_8
inst✝⁶ : NormedAddCommGroup F₁
inst✝⁵ : NormedSpace 𝕜 F₁
inst✝⁴ : NormedSpace ℝ F₁
inst✝³ : NormedAddCommGroup F₂
inst✝² : NormedSpace 𝕜 F₂
inst✝¹ : NormedAddCommGroup F₃
inst✝ : NormedSpace 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : LocallyIntegrableOn φ (↑Ω) μ
f : 𝓓^{n}(Ω, F₁)
this : IntegrableOn (fun x ↦ (B (f x)) (φ x)) (tsupport ⇑f) μ
x : E
hx : x ∈ support fun x ↦ (B (f x)) (φ x)
hfx : f x = 0
⊢ (fun x ↦ (B (f x)) (φ x)) x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : (↑T).IsSymmetric
M : ℝ := ⨆ x, |T.rayleighQuotient x|
nonneg : 0 ≤ M
x : E
hM : |T.reApplyInnerSelf x| / ‖x‖ ^ 2 ≤ M
hx : 0 < ‖x‖ ^ 2
⊢ |re ⟪T x, x⟫_𝕜| ≤ M * ‖x‖ ^ 2

Tactic:
reApplyInnerSelf,

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : (↑T).IsSymmetric
M : ℝ := ⨆ x, |T.rayleighQuotient x|
nonneg : 0 ≤ M
x : E
hM : |re ⟪T x, x⟫_𝕜| / ‖x‖ ^ 2 ≤ M
hx : 0 < ‖x‖ ^ 2
⊢ |re ⟪T x, x⟫_𝕜| ≤ M * ‖x‖ ^ 2
Module: Mathlib.Analysis.Distribution.TestFunction

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
m : MeasurableSpace E
inst✝⁷ : OpensMeasurableSpace E
F₁ : Type u_6
F₂ : Type u_7
F₃ : Type u_8
inst✝⁶ : NormedAddCommGroup F₁
inst✝⁵ : NormedSpace 𝕜 F₁
inst✝⁴ : NormedSpace ℝ F₁
inst✝³ : NormedAddCommGroup F₂
inst✝² : NormedSpace 𝕜 F₂
inst✝¹ : NormedAddCommGroup F₃
inst✝ : NormedSpace 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : LocallyIntegrableOn φ (↑Ω) μ
f : 𝓓^{n}(Ω, F₁)
this : IntegrableOn (fun x ↦ (B (f x)) (φ x)) (tsupport ⇑f) μ
⊢ Integrable (fun x ↦ (B (f x)) (φ x)) μ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : (↑T).IsSymmetric
M : ℝ := ⨆ x, |T.rayleighQuotient x|
nonneg : 0 ≤ M
x : E
⊢ |re ⟪T x, x⟫_𝕜| ≤ M * ‖x‖ ^ 2

Tactic:
by

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

Goal state before:
pp: H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y | 1 / 2 < y}
ht : (Set.range fun x ↦ 1 + ‖x‖ ^ 2) ⊆ t
hdiff : ContDiffOn ℝ ∞ (fun x ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r ((↑N - r) * Real.log 2 / Real.log (3 / 2)) ≤ ↑k
hk₁ : r ≤ ↑k
hk₂ : Real.log 2 * (↑N - r) ≤ Real.log (3 / 2) * ↑k
n : ℕ
hn : n ≤ N
x : ℝ
hx : x ∈ t
this : ContDiffAt ℝ (↑n) (fun x ↦ x ^ r) x
⊢ n ∈ Finset.range (N + 1)

Tactic:
by

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

Goal state before:
pp: H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y | 1 / 2 < y}
ht : (Set.range fun x ↦ 1 + ‖x‖ ^ 2) ⊆ t
hdiff : ContDiffOn ℝ ∞ (fun x ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r ((↑N - r) * Real.log 2 / Real.log (3 / 2)) ≤ ↑k
hk₁ : r ≤ ↑k
hk₂ : Real.log 2 * (↑N - r) ≤ Real.log (3 / 2) * ↑k
n : ℕ
hn : n ≤ N
x : ℝ
hx : x ∈ t
this✝ : ContDiffAt ℝ (↑n) (fun x ↦ x ^ r) x
this : n ∈ Finset.range (N + 1)
x✝¹ : ℕ
x✝ : x✝¹ ∈ Finset.range (N + 1)
⊢ 0 ≤ ‖Polynomial.eval r (descPochhammer ℝ x✝¹)‖

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
m : MeasurableSpace E
inst✝⁷ : OpensMeasurableSpace E
F₁ : Type u_6
F₂ : Type u_7
F₃ : Type u_8
inst✝⁶ : NormedAddCommGroup F₁
inst✝⁵ : NormedSpace 𝕜 F₁
inst✝⁴ : NormedSpace ℝ F₁
inst✝³ : NormedAddCommGroup F₂
inst✝² : NormedSpace 𝕜 F₂
inst✝¹ : NormedAddCommGroup F₃
inst✝ : NormedSpace 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : LocallyIntegrableOn φ (↑Ω) μ
f : 𝓓^{n}(Ω, F₁)
⊢ Integrable (fun x ↦ (B (f x)) (φ x)) μ

Tactic:
by

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

Goal state before:
pp: H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y | 1 / 2 < y}
ht : (Set.range fun x ↦ 1 + ‖x‖ ^ 2) ⊆ t
hdiff : ContDiffOn ℝ ∞ (fun x ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r ((↑N - r) * Real.log 2 / Real.log (3 / 2)) ≤ ↑k
hk₁ : r ≤ ↑k
hk₂ : Real.log 2 * (↑N - r) ≤ Real.log (3 / 2) * ↑k
n : ℕ
hn : n ≤ N
x : ℝ
hx : x ∈ t
this : ContDiffAt ℝ (↑n) (fun x ↦ x ^ r) x
⊢ 1 / 2 < x

Tactic:
by

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

Goal state before:
pp: E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
n : ℕ∞
m : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
f : 𝓓^{n}(Ω, F)
H : IntegrableOn (fun x ↦ 1) (tsupport ⇑f) μ
this : IntegrableOn (⇑(1 • f)) (tsupport ⇑f) μ
⊢ IntegrableOn (⇑f) (tsupport ⇑f) μ

Tactic:
by

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

Goal state before:
pp: H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y | 1 / 2 < y}
ht : (Set.range fun x ↦ 1 + ‖x‖ ^ 2) ⊆ t
hdiff : ContDiffOn ℝ ∞ (fun x ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r ((↑N - r) * Real.log 2 / Real.log (3 / 2)) ≤ ↑k
hk₁ : r ≤ ↑k
hk₂ : Real.log 2 * (↑N - r) ≤ Real.log (3 / 2) * ↑k
n : ℕ
hn : n ≤ N
x : ℝ
hx : x ∈ t
this : ContDiffAt ℝ (↑n) (fun x ↦ x ^ r) x
hx' : 1 / 2 < x
⊢ 0 < 1 / 2

Tactic:
by

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

Goal state before:
pp: E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
n : ℕ∞
m : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
H : LocallyIntegrableOn (fun x ↦ 1) (↑Ω) μ
f : 𝓓^{n}(Ω, F)
⊢ Integrable (⇑f) μ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : (↑T).IsSymmetric
⊢ ‖T‖ = ⨆ x, |T.rayleighQuotient x|

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
t : ℝ
ht : 0 < t
hT' : (algebraMap ℝ 𝕜) t ∈ resolventSet 𝕜 T
hT0 : T = 0
⊢ t ^ 2 / (2 * t) > 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
t : ℝ
ht : 0 < t
hT' : (algebraMap ℝ 𝕜) t ∈ resolventSet 𝕜 T
hT0 : T = 0
⊢ ∀ (x : E), T.rayleighQuotient x ≤ (t ^ 2 + ‖T‖ ^ 2) / (2 * t) - t ^ 2 / (2 * t)

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
𝕂 : Type u_2
inst✝²⁰ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹⁹ : NormedAddCommGroup E
inst✝¹⁸ : NormedSpace ℝ E
Ω Ω₁ Ω₂ : Opens E
F : Type u_4
inst✝¹⁷ : NormedAddCommGroup F
inst✝¹⁶ : NormedSpace ℝ F
inst✝¹⁵ : NormedSpace 𝕜 F
F' : Type u_5
inst✝¹⁴ : NormedAddCommGroup F'
inst✝¹³ : NormedSpace ℝ F'
inst✝¹² : NormedSpace 𝕜 F'
n n₁ n₂ k : ℕ∞
m : MeasurableSpace E
inst✝¹¹ : OpensMeasurableSpace E
F₁ : Type u_6
F₂ : Type u_7
F₃ : Type u_8
inst✝¹⁰ : NormedAddCommGroup F₁
inst✝⁹ : NormedSpace 𝕜 F₁
inst✝⁸ : NormedSpace ℝ F₁
inst✝⁷ : NormedAddCommGroup F₂
inst✝⁶ : NormedSpace 𝕜 F₂
inst✝⁵ : NormedAddCommGroup F₃
inst✝⁴ : NormedSpace 𝕜 F₃
inst✝³ : Algebra ℝ 𝕜
inst✝² : IsScalarTower ℝ 𝕜 F₁
inst✝¹ : NormedSpace ℝ F₃
inst✝ : IsScalarTower ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
K : Compacts E
K_sub_Ω : ↑K ⊆ ↑Ω
f : 𝓓^{n}_{K}(E, F₁)
⊢ (if LocallyIntegrableOn φ (↑Ω) μ then ∫ (x : E), (B ((ofSupportedIn K_sub_Ω f) x)) (φ x) ∂μ else 0) =
    (if LocallyIntegrableOn φ (↑Ω) μ then ContDiffMapSupportedIn.integralAgainstBilinCLM B μ φ else 0) f

Tactic:
by

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

Goal state before:
pp: H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y | 1 / 2 < y}
ht : (Set.range fun x ↦ 1 + ‖x‖ ^ 2) ⊆ t
hdiff : ContDiffOn ℝ ∞ (fun x ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r ((↑N - r) * Real.log 2 / Real.log (3 / 2)) ≤ ↑k
hk₁ : r ≤ ↑k
hk₂ : Real.log 2 * (↑N - r) ≤ Real.log (3 / 2) * ↑k
n : ℕ
hn : n ≤ N
x : ℝ
hx : x ∈ t
this : ContDiffAt ℝ (↑n) (fun x ↦ x ^ r) x
hx' : 1 / 2 < x
hx'' : 0 < x
h : 0 ≤ r - ↑n
⊢ ↑k ≤ ↑k + ↑n

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
m : MeasurableSpace E
inst✝¹¹ : OpensMeasurableSpace E
F₁ : Type u_6
F₂ : Type u_7
F₃ : Type u_8
inst✝¹⁰ : NormedAddCommGroup F₁
inst✝⁹ : NormedSpace 𝕜 F₁
inst✝⁸ : NormedSpace ℝ F₁
inst✝⁷ : NormedAddCommGroup F₂
inst✝⁶ : NormedSpace 𝕜 F₂
inst✝⁵ : NormedAddCommGroup F₃
inst✝⁴ : NormedSpace 𝕜 F₃
inst✝³ : Algebra ℝ 𝕜
inst✝² : IsScalarTower ℝ 𝕜 F₁
inst✝¹ : NormedSpace ℝ F₃
inst✝ : IsScalarTower ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : LocallyIntegrableOn φ (↑Ω) μ
f : 𝓓^{n}(Ω, F₁)
⊢ (integralAgainstBilinCLM B μ φ) f = ∫ (x : E), (B (f x)) (φ x) ∂μ

Tactic:
by

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

Goal state before:
pp: H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y | 1 / 2 < y}
ht : (Set.range fun x ↦ 1 + ‖x‖ ^ 2) ⊆ t
hdiff : ContDiffOn ℝ ∞ (fun x ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r ((↑N - r) * Real.log 2 / Real.log (3 / 2)) ≤ ↑k
hk₁ : r ≤ ↑k
hk₂ : Real.log 2 * (↑N - r) ≤ Real.log (3 / 2) * ↑k
n : ℕ
hn : n ≤ N
x : ℝ
hx : x ∈ t
this : ContDiffAt ℝ (↑n) (fun x ↦ x ^ r) x
hx' : 1 / 2 < x
hx'' : 0 < x
h : 0 ≤ r - ↑n
⊢ r - ↑n ≤ ↑k

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
t : ℝ
ht : 0 < t
hT' : (algebraMap ℝ 𝕜) t ∈ resolventSet 𝕜 T
hT0 : ¬T = 0
c : ℝ
hc0 : c > 0
hc : ∀ (x : E), c * ‖x‖ ≤ ‖((algebraMap 𝕜 (E →L[𝕜] E)) ((algebraMap ℝ 𝕜) t) - T) x‖
⊢ min (c ^ 2 / (2 * t)) ((t ^ 2 + ‖T‖ ^ 2) / (2 * t)) > 0

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
m : MeasurableSpace E
inst✝¹¹ : OpensMeasurableSpace E
F₁ : Type u_6
F₂ : Type u_7
F₃ : Type u_8
inst✝¹⁰ : NormedAddCommGroup F₁
inst✝⁹ : NormedSpace 𝕜 F₁
inst✝⁸ : NormedSpace ℝ F₁
inst✝⁷ : NormedAddCommGroup F₂
inst✝⁶ : NormedSpace 𝕜 F₂
inst✝⁵ : NormedAddCommGroup F₃
inst✝⁴ : NormedSpace 𝕜 F₃
inst✝³ : Algebra ℝ 𝕜
inst✝² : IsScalarTower ℝ 𝕜 F₁
inst✝¹ : NormedSpace ℝ F₃
inst✝ : IsScalarTower ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : ¬LocallyIntegrableOn φ (↑Ω) μ
⊢ integralAgainstBilinCLM B μ φ = 0

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
m : MeasurableSpace E
inst✝¹¹ : OpensMeasurableSpace E
F₁ : Type u_6
F₂ : Type u_7
F₃ : Type u_8
inst✝¹⁰ : NormedAddCommGroup F₁
inst✝⁹ : NormedSpace 𝕜 F₁
inst✝⁸ : NormedSpace ℝ F₁
inst✝⁷ : NormedAddCommGroup F₂
inst✝⁶ : NormedSpace 𝕜 F₂
inst✝⁵ : NormedAddCommGroup F₃
inst✝⁴ : NormedSpace 𝕜 F₃
inst✝³ : Algebra ℝ 𝕜
inst✝² : IsScalarTower ℝ 𝕜 F₁
inst✝¹ : NormedSpace ℝ F₃
inst✝ : IsScalarTower ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : LocallyIntegrableOn φ (↑Ω) μ
K : Compacts E
K_sub_Ω : ↑K ⊆ ↑Ω
f : 𝓓^{n}_{K}(E, F₁)
⊢ (integralAgainstBilinCLM B μ φ) (ofSupportedIn K_sub_Ω f) = (ContDiffMapSupportedIn.integralAgainstBilinCLM B μ φ) f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Compact.Basic

Goal state before:
pp: M₁ : Type u_2
M₂ : Type u_3
inst✝³ : TopologicalSpace M₁
inst✝² : AddCommMonoid M₁
inst✝¹ : TopologicalSpace M₂
inst✝ : T2Space M₂
f : M₁ → M₂
⊢ IsCompactOperator f ↔ ∃ V ∈ 𝓝 0, IsCompact (closure[inst✝¹] (f '' V))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Compact.Basic

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜₁
inst✝⁷ : SeminormedRing 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁶ : TopologicalSpace M₁
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : TopologicalSpace M₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module 𝕜₁ M₁
inst✝¹ : Module 𝕜₂ M₂
inst✝ : ContinuousConstSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator ⇑f
S : Set M₁
hS : IsVonNBounded 𝕜₁ S
K : Set M₂
hK : IsCompact K
hKf : ⇑f ⁻¹' K ∈ 𝓝 0
r : ℝ
hr : r > 0
hrS : ∀ (c : 𝕜₁), r ≤ ‖c‖ → S ⊆ c • ⇑f ⁻¹' K
c : 𝕜₁
hc : r < ‖c‖
this : c ≠ 0 := ne_zero_of_norm_ne_zero (Ne.symm (LT.lt.ne (LT.lt.trans hr hc)))
⊢ ⇑f '' S ⊆ σ₁₂ c • K

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Compact.Basic

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜₁
inst✝⁶ : SeminormedRing 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁵ : SeminormedAddCommGroup M₁
inst✝⁴ : TopologicalSpace M₂
inst✝³ : AddCommMonoid M₂
inst✝² : NormedSpace 𝕜₁ M₁
inst✝¹ : Module 𝕜₂ M₂
inst✝ : ContinuousConstSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator ⇑f
S : Set M₁
hS : Bornology.IsBounded S
⊢ IsVonNBounded 𝕜₁ S

Tactic:
by

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

Goal state before:
pp: H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y | 1 / 2 < y}
ht : (Set.range fun x ↦ 1 + ‖x‖ ^ 2) ⊆ t
hdiff : ContDiffOn ℝ ∞ (fun x ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r ((↑N - r) * Real.log 2 / Real.log (3 / 2)) ≤ ↑k
hk₁ : r ≤ ↑k
hk₂ : Real.log 2 * (↑N - r) ≤ Real.log (3 / 2) * ↑k
n : ℕ
hn : n ≤ N
x : ℝ
hx : x ∈ t
this✝ : ContDiffAt ℝ (↑n) (fun x ↦ x ^ r) x
hx' : 1 / 2 < x
hx'' : 0 < x
h : 0 ≤ r - ↑n
this : r - ↑n ≤ ↑k
⊢ 0 ≤ |x|

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Compact.Basic

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜₁
inst✝⁷ : SeminormedRing 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁶ : SeminormedAddCommGroup M₁
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : NormedSpace 𝕜₁ M₁
inst✝² : Module 𝕜₂ M₂
inst✝¹ : ContinuousConstSMul 𝕜₂ M₂
inst✝ : T2Space M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator ⇑f
S : Set M₁
hS : Bornology.IsBounded S
⊢ IsVonNBounded 𝕜₁ S

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Compact.Basic

Goal state before:
pp: M₁ : Type u_3
M₂ : Type u_4
inst✝⁶ : TopologicalSpace M₁
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : TopologicalSpace M₂
inst✝³ : AddCommMonoid M₂
S : Type u_6
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M₂
inst✝ : ContinuousConstSMul S M₂
f : M₁ → M₂
c : Sˣ
h : IsCompactOperator (c • f)
⊢ IsCompactOperator f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Compact.Basic

Goal state before:
pp: M₁ : Type u_3
M₂ : Type u_4
inst✝⁶ : TopologicalSpace M₁
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : TopologicalSpace M₂
inst✝³ : AddCommMonoid M₂
S : Type u_6
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M₂
inst✝ : ContinuousConstSMul S M₂
f : M₁ → M₂
c : S
hc : IsUnit c
⊢ IsCompactOperator (c • f) ↔ IsCompactOperator f

Tactic:
by

Goal state after: