mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝¹⁸ : RCLike 𝕜
inst✝¹⁷ : NonUnitalRing A
inst✝¹⁶ : TopologicalSpace A
inst✝¹⁵ : Module 𝕜 A
inst✝¹⁴ : StarRing A
inst✝¹³ : PartialOrder A
inst✝¹² : StarOrderedRing A
inst✝¹¹ : IsScalarTower 𝕜 A A
inst✝¹⁰ : SMulCommClass 𝕜 A A
inst✝⁹ : Module ℝ A
inst✝⁸ : SMulCommClass ℝ A A
inst✝⁷ : IsScalarTower ℝ A A
inst✝⁶ : NonnegSpectrumClass ℝ A
inst✝⁵ : IsTopologicalRing A
inst✝⁴ : T2Space A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : StarModule 𝕜 A
inst✝¹ : StarModule ℝ A
inst✝ : IsScalarTower ℝ 𝕜 A
r : 𝕜
a : A
⊢ abs (r • a) = abs (‖r‖ • a)

pp: 𝕜 : Type u_1
A : Type u_2
inst✝¹⁸ : RCLike 𝕜
inst✝¹⁷ : NonUnitalRing A
inst✝¹⁶ : TopologicalSpace A
inst✝¹⁵ : Module 𝕜 A
inst✝¹⁴ : StarRing A
inst✝¹³ : PartialOrder A
inst✝¹² : StarOrderedRing A
inst✝¹¹ : IsScalarTower 𝕜 A A
inst✝¹⁰ : SMulCommClass 𝕜 A A
inst✝⁹ : Module ℝ A
inst✝⁸ : SMulCommClass ℝ A A
inst✝⁷ : IsScalarTower ℝ A A
inst✝⁶ : NonnegSpectrumClass ℝ A
inst✝⁵ : IsTopologicalRing A
inst✝⁴ : T2Space A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : StarModule 𝕜 A
inst✝¹ : StarModule ℝ A
inst✝ : IsScalarTower ℝ 𝕜 A
r : 𝕜
a : A
⊢ abs (‖r‖ • a) = ‖r‖ • abs a

Tactic:
·

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝¹⁸ : RCLike 𝕜
inst✝¹⁷ : NonUnitalRing A
inst✝¹⁶ : TopologicalSpace A
inst✝¹⁵ : Module 𝕜 A
inst✝¹⁴ : StarRing A
inst✝¹³ : PartialOrder A
inst✝¹² : StarOrderedRing A
inst✝¹¹ : IsScalarTower 𝕜 A A
inst✝¹⁰ : SMulCommClass 𝕜 A A
inst✝⁹ : Module ℝ A
inst✝⁸ : SMulCommClass ℝ A A
inst✝⁷ : IsScalarTower ℝ A A
inst✝⁶ : NonnegSpectrumClass ℝ A
inst✝⁵ : IsTopologicalRing A
inst✝⁴ : T2Space A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : StarModule 𝕜 A
inst✝¹ : StarModule ℝ A
inst✝ : IsScalarTower ℝ 𝕜 A
r : 𝕜
a : A
⊢ abs (r • a) = abs (‖r‖ • a)
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: case e'_2.e'_6
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
x✝ : α
⊢ ‖f x✝‖ ^ 2 = ‖f x✝‖ ^ ENNReal.toReal 2

pp: case e'_2.e'_7
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
⊢ 1 = 2 / 2

Tactic:
·

Goal state after:
case e'_2.e'_6
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
x✝ : α
⊢ ‖f x✝‖ ^ 2 = ‖f x✝‖ ^ ENNReal.toReal 2
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: case e'_2.e'_7
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
⊢ 1 = 2 / 2

Tactic:
·

Goal state after:
case e'_2.e'_7
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
⊢ 1 = 2 / 2
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝¹⁸ : RCLike 𝕜
inst✝¹⁷ : NonUnitalRing A
inst✝¹⁶ : TopologicalSpace A
inst✝¹⁵ : Module 𝕜 A
inst✝¹⁴ : StarRing A
inst✝¹³ : PartialOrder A
inst✝¹² : StarOrderedRing A
inst✝¹¹ : IsScalarTower 𝕜 A A
inst✝¹⁰ : SMulCommClass 𝕜 A A
inst✝⁹ : Module ℝ A
inst✝⁸ : SMulCommClass ℝ A A
inst✝⁷ : IsScalarTower ℝ A A
inst✝⁶ : NonnegSpectrumClass ℝ A
inst✝⁵ : IsTopologicalRing A
inst✝⁴ : T2Space A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : StarModule 𝕜 A
inst✝¹ : StarModule ℝ A
inst✝ : IsScalarTower ℝ 𝕜 A
r : 𝕜
a : A
⊢ abs (‖r‖ • a) = ‖r‖ • abs a

Tactic:
·

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝¹⁸ : RCLike 𝕜
inst✝¹⁷ : NonUnitalRing A
inst✝¹⁶ : TopologicalSpace A
inst✝¹⁵ : Module 𝕜 A
inst✝¹⁴ : StarRing A
inst✝¹³ : PartialOrder A
inst✝¹² : StarOrderedRing A
inst✝¹¹ : IsScalarTower 𝕜 A A
inst✝¹⁰ : SMulCommClass 𝕜 A A
inst✝⁹ : Module ℝ A
inst✝⁸ : SMulCommClass ℝ A A
inst✝⁷ : IsScalarTower ℝ A A
inst✝⁶ : NonnegSpectrumClass ℝ A
inst✝⁵ : IsTopologicalRing A
inst✝⁴ : T2Space A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : StarModule 𝕜 A
inst✝¹ : StarModule ℝ A
inst✝ : IsScalarTower ℝ 𝕜 A
r : 𝕜
a : A
⊢ abs (‖r‖ • a) = ‖r‖ • abs a
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: case inl
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : NonUnitalRing A
inst✝¹⁴ : TopologicalSpace A
inst✝¹³ : Module 𝕜 A
inst✝¹² : StarRing A
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : StarOrderedRing A
inst✝⁹ : IsScalarTower 𝕜 A A
inst✝⁸ : SMulCommClass 𝕜 A A
inst✝⁷ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝⁶ : Module ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : IsTopologicalRing A
inst✝¹ : T2Space A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
f : 𝕜 → 𝕜
a : A
ha : p a
hf : ContinuousOn f ((fun z ↦ ↑‖z‖) '' quasispectrum 𝕜 a)
hf0 : f 0 = 0
⊢ cfcₙ (fun x ↦ f ↑‖x‖) a = cfcₙ f (abs a)

pp: case inr
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : NonUnitalRing A
inst✝¹⁴ : TopologicalSpace A
inst✝¹³ : Module 𝕜 A
inst✝¹² : StarRing A
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : StarOrderedRing A
inst✝⁹ : IsScalarTower 𝕜 A A
inst✝⁸ : SMulCommClass 𝕜 A A
inst✝⁷ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝⁶ : Module ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : IsTopologicalRing A
inst✝¹ : T2Space A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
f : 𝕜 → 𝕜
a : A
ha : p a
hf : ContinuousOn f ((fun z ↦ ↑‖z‖) '' quasispectrum 𝕜 a)
hf0 : ¬f 0 = 0
⊢ cfcₙ (fun x ↦ f ↑‖x‖) a = cfcₙ f (abs a)

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : NonUnitalRing A
inst✝¹⁴ : TopologicalSpace A
inst✝¹³ : Module 𝕜 A
inst✝¹² : StarRing A
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : StarOrderedRing A
inst✝⁹ : IsScalarTower 𝕜 A A
inst✝⁸ : SMulCommClass 𝕜 A A
inst✝⁷ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝⁶ : Module ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : IsTopologicalRing A
inst✝¹ : T2Space A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
f : 𝕜 → 𝕜
a : A
ha : p a
hf : ContinuousOn f ((fun z ↦ ↑‖z‖) '' quasispectrum 𝕜 a)
hf0 : f 0 = 0
⊢ cfcₙ (fun x ↦ f ↑‖x‖) a = cfcₙ f (abs a)
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: case refine_1
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
h : ∀ (x : α), ‖⟪↑↑f x, ↑↑g x⟫‖ ≤ ‖‖↑↑f x‖ ^ 2 + ‖↑↑g x‖ ^ 2‖
⊢ AEStronglyMeasurable (fun a ↦ ‖↑↑f a‖ ^ 2) μ

pp: case refine_2
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
h : ∀ (x : α), ‖⟪↑↑f x, ↑↑g x⟫‖ ≤ ‖‖↑↑f x‖ ^ 2 + ‖↑↑g x‖ ^ 2‖
⊢ AEStronglyMeasurable (fun a ↦ ‖↑↑g a‖ ^ 2) μ

pp: case refine_3
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
h : ∀ (x : α), ‖⟪↑↑f x, ↑↑g x⟫‖ ≤ ‖‖↑↑f x‖ ^ 2 + ‖↑↑g x‖ ^ 2‖
⊢ eLpNorm (fun a ↦ ‖↑↑f a‖ ^ 2) 1 μ + eLpNorm (fun a ↦ ‖↑↑g a‖ ^ 2) 1 μ < ∞

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
h : ∀ (x : α), ‖⟪↑↑f x, ↑↑g x⟫‖ ≤ ‖‖↑↑f x‖ ^ 2 + ‖↑↑g x‖ ^ 2‖
⊢ AEStronglyMeasurable (fun a ↦ ‖↑↑f a‖ ^ 2) μ
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: case refine_2
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
h : ∀ (x : α), ‖⟪↑↑f x, ↑↑g x⟫‖ ≤ ‖‖↑↑f x‖ ^ 2 + ‖↑↑g x‖ ^ 2‖
⊢ AEStronglyMeasurable (fun a ↦ ‖↑↑g a‖ ^ 2) μ

pp: case refine_3
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
h : ∀ (x : α), ‖⟪↑↑f x, ↑↑g x⟫‖ ≤ ‖‖↑↑f x‖ ^ 2 + ‖↑↑g x‖ ^ 2‖
⊢ eLpNorm (fun a ↦ ‖↑↑f a‖ ^ 2) 1 μ + eLpNorm (fun a ↦ ‖↑↑g a‖ ^ 2) 1 μ < ∞

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
h : ∀ (x : α), ‖⟪↑↑f x, ↑↑g x⟫‖ ≤ ‖‖↑↑f x‖ ^ 2 + ‖↑↑g x‖ ^ 2‖
⊢ AEStronglyMeasurable (fun a ↦ ‖↑↑g a‖ ^ 2) μ
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: case inr
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : NonUnitalRing A
inst✝¹⁴ : TopologicalSpace A
inst✝¹³ : Module 𝕜 A
inst✝¹² : StarRing A
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : StarOrderedRing A
inst✝⁹ : IsScalarTower 𝕜 A A
inst✝⁸ : SMulCommClass 𝕜 A A
inst✝⁷ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝⁶ : Module ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : IsTopologicalRing A
inst✝¹ : T2Space A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
f : 𝕜 → 𝕜
a : A
ha : p a
hf : ContinuousOn f ((fun z ↦ ↑‖z‖) '' quasispectrum 𝕜 a)
hf0 : ¬f 0 = 0
⊢ cfcₙ (fun x ↦ f ↑‖x‖) a = cfcₙ f (abs a)

Tactic:
·

Goal state after:
case inr
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : NonUnitalRing A
inst✝¹⁴ : TopologicalSpace A
inst✝¹³ : Module 𝕜 A
inst✝¹² : StarRing A
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : StarOrderedRing A
inst✝⁹ : IsScalarTower 𝕜 A A
inst✝⁸ : SMulCommClass 𝕜 A A
inst✝⁷ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝⁶ : Module ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : IsTopologicalRing A
inst✝¹ : T2Space A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
f : 𝕜 → 𝕜
a : A
ha : p a
hf : ContinuousOn f ((fun z ↦ ↑‖z‖) '' quasispectrum 𝕜 a)
hf0 : ¬f 0 = 0
⊢ cfcₙ (fun x ↦ f ↑‖x‖) a = cfcₙ f (abs a)
Module: Mathlib.Geometry.Manifold.SmoothApprox

Goal state before:
pp: case pos
E : Type u_1
F : Type u_2
H : Type u_3
M : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f : M → F
ε : M → ℝ
n : ℕ∞
f_cont : Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
ε_cont : Continuous[inst✝⁴, _] ε
ε_pos : ∀ (x : M), 0 < ε x
S U : Set M
hS : IsClosed[inst✝⁴] S
hU : U ∈ 𝓝ˢ S
hfU : ContMDiffOn I 𝓘(ℝ, F) (↑n) f U
dist_f_f : ∀ (x : M), dist (f x) (f x) < ε x
t : M → Set F := fun x ↦ {y | dist y (f x) < ε x ∧ (x ∈ S → y = f x) ∧ (f x = 0 → y = 0)}
t_conv : ∀ (x : M), Convex ℝ (t x)
x : M
hx : x ∈ S
⊢ ∃ U ∈ 𝓝 x, ∃ g, ContMDiffOn I 𝓘(ℝ, F) (↑n) g U ∧ ∀ y ∈ U, g y ∈ t y

pp: case neg
E : Type u_1
F : Type u_2
H : Type u_3
M : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f : M → F
ε : M → ℝ
n : ℕ∞
f_cont : Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
ε_cont : Continuous[inst✝⁴, _] ε
ε_pos : ∀ (x : M), 0 < ε x
S U : Set M
hS : IsClosed[inst✝⁴] S
hU : U ∈ 𝓝ˢ S
hfU : ContMDiffOn I 𝓘(ℝ, F) (↑n) f U
dist_f_f : ∀ (x : M), dist (f x) (f x) < ε x
t : M → Set F := fun x ↦ {y | dist y (f x) < ε x ∧ (x ∈ S → y = f x) ∧ (f x = 0 → y = 0)}
t_conv : ∀ (x : M), Convex ℝ (t x)
x : M
hx : x ∉ S
⊢ ∃ U ∈ 𝓝 x, ∃ g, ContMDiffOn I 𝓘(ℝ, F) (↑n) g U ∧ ∀ y ∈ U, g y ∈ t y

Tactic:
·

Goal state after:
case pos
E : Type u_1
F : Type u_2
H : Type u_3
M : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f : M → F
ε : M → ℝ
n : ℕ∞
f_cont : Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
ε_cont : Continuous[inst✝⁴, _] ε
ε_pos : ∀ (x : M), 0 < ε x
S U : Set M
hS : IsClosed[inst✝⁴] S
hU : U ∈ 𝓝ˢ S
hfU : ContMDiffOn I 𝓘(ℝ, F) (↑n) f U
dist_f_f : ∀ (x : M), dist (f x) (f x) < ε x
t : M → Set F := fun x ↦ {y | dist y (f x) < ε x ∧ (x ∈ S → y = f x) ∧ (f x = 0 → y = 0)}
t_conv : ∀ (x : M), Convex ℝ (t x)
x : M
hx : x ∈ S
⊢ ∃ U ∈ 𝓝 x, ∃ g, ContMDiffOn I 𝓘(ℝ, F) (↑n) g U ∧ ∀ y ∈ U, g y ∈ t y
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: case hf
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ 0 ≤ᵐ[μ] fun x ↦ ‖↑↑f x‖ ^ 2

pp: case hfm
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ AEStronglyMeasurable (fun x ↦ ‖↑↑f x‖ ^ 2) μ

pp: α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ (∫⁻ (a : α), ENNReal.ofReal (‖↑↑f a‖ ^ 2) ∂μ).toReal = (∫⁻ (a : α), ↑(‖↑↑f a‖₊ ^ 2) ∂μ).toReal

Tactic:
·

Goal state after:
case hf
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ 0 ≤ᵐ[μ] fun x ↦ ‖↑↑f x‖ ^ 2
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
i : ℕ
f : 𝓓^{n₁}_{K₁}(E, F)
H : n₂ ≤ n₁ ∧ K₁ ≤ K₂
⊢ (ContDiffMapSupportedIn.seminorm 𝕜 E F n₂ K₂ i) ((monoLM 𝕜) f) ≤ (ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ i) f

pp: case neg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
i : ℕ
f : 𝓓^{n₁}_{K₁}(E, F)
H : ¬(n₂ ≤ n₁ ∧ K₁ ≤ K₂)
⊢ (ContDiffMapSupportedIn.seminorm 𝕜 E F n₂ K₂ i) ((monoLM 𝕜) f) ≤ (ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ i) f

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
i : ℕ
f : 𝓓^{n₁}_{K₁}(E, F)
H : n₂ ≤ n₁ ∧ K₁ ≤ K₂
⊢ (ContDiffMapSupportedIn.seminorm 𝕜 E F n₂ K₂ i) ((monoLM 𝕜) f) ≤ (ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ i) f
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: case hfm
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ AEStronglyMeasurable (fun x ↦ ‖↑↑f x‖ ^ 2) μ

pp: α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ (∫⁻ (a : α), ENNReal.ofReal (‖↑↑f a‖ ^ 2) ∂μ).toReal = (∫⁻ (a : α), ↑(‖↑↑f a‖₊ ^ 2) ∂μ).toReal

Tactic:
·

Goal state after:
case hfm
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ AEStronglyMeasurable (fun x ↦ ‖↑↑f x‖ ^ 2) μ
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
i : ℕ
f : 𝓓^{n₁}_{K₁}(E, F)
H : ¬(n₂ ≤ n₁ ∧ K₁ ≤ K₂)
⊢ (ContDiffMapSupportedIn.seminorm 𝕜 E F n₂ K₂ i) ((monoLM 𝕜) f) ≤ (ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ i) f

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
i : ℕ
f : 𝓓^{n₁}_{K₁}(E, F)
H : ¬(n₂ ≤ n₁ ∧ K₁ ≤ K₂)
⊢ (ContDiffMapSupportedIn.seminorm 𝕜 E F n₂ K₂ i) ((monoLM 𝕜) f) ≤ (ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ i) f
Module: Mathlib.Geometry.Manifold.SmoothApprox

Goal state before:
pp: case neg
E : Type u_1
F : Type u_2
H : Type u_3
M : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f : M → F
ε : M → ℝ
n : ℕ∞
f_cont : Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
ε_cont : Continuous[inst✝⁴, _] ε
ε_pos : ∀ (x : M), 0 < ε x
S U : Set M
hS : IsClosed[inst✝⁴] S
hU : U ∈ 𝓝ˢ S
hfU : ContMDiffOn I 𝓘(ℝ, F) (↑n) f U
dist_f_f : ∀ (x : M), dist (f x) (f x) < ε x
t : M → Set F := fun x ↦ {y | dist y (f x) < ε x ∧ (x ∈ S → y = f x) ∧ (f x = 0 → y = 0)}
t_conv : ∀ (x : M), Convex ℝ (t x)
x : M
hx : x ∉ S
⊢ ∃ U ∈ 𝓝 x, ∃ g, ContMDiffOn I 𝓘(ℝ, F) (↑n) g U ∧ ∀ y ∈ U, g y ∈ t y

Tactic:
·

Goal state after:
case neg
E : Type u_1
F : Type u_2
H : Type u_3
M : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f : M → F
ε : M → ℝ
n : ℕ∞
f_cont : Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
ε_cont : Continuous[inst✝⁴, _] ε
ε_pos : ∀ (x : M), 0 < ε x
S U : Set M
hS : IsClosed[inst✝⁴] S
hU : U ∈ 𝓝ˢ S
hfU : ContMDiffOn I 𝓘(ℝ, F) (↑n) f U
dist_f_f : ∀ (x : M), dist (f x) (f x) < ε x
t : M → Set F := fun x ↦ {y | dist y (f x) < ε x ∧ (x ∈ S → y = f x) ∧ (f x = 0 → y = 0)}
t_conv : ∀ (x : M), Convex ℝ (t x)
x : M
hx : x ∉ S
⊢ ∃ U ∈ 𝓝 x, ∃ g, ContMDiffOn I 𝓘(ℝ, F) (↑n) g U ∧ ∀ y ∈ U, g y ∈ t y
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
h_two : ENNReal.toReal 2 = 2
⊢ eLpNorm (↑↑f) 2 μ ^ 2 = ∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ

pp: α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
h_two : ENNReal.toReal 2 = 2
⊢ ∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ ≠ ∞

Tactic:
·

Goal state after:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
h_two : ENNReal.toReal 2 = 2
⊢ eLpNorm (↑↑f) 2 μ ^ 2 = ∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n k : ℕ∞
K : Compacts E
i : ℕ
f : 𝓓^{n}_{K}(E, F)
hk : k + 1 ≤ n
⊢ (ContDiffMapSupportedIn.seminorm 𝕜 E (E →L[ℝ] F) k K i) ((fderivLM 𝕜 n k) f) ≤
    (ContDiffMapSupportedIn.seminorm 𝕜 E F n K (i + 1)) f

pp: case neg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n k : ℕ∞
K : Compacts E
i : ℕ
f : 𝓓^{n}_{K}(E, F)
hk : n < k + 1
⊢ (ContDiffMapSupportedIn.seminorm 𝕜 E (E →L[ℝ] F) k K i) ((fderivLM 𝕜 n k) f) ≤
    (ContDiffMapSupportedIn.seminorm 𝕜 E F n K (i + 1)) f

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n k : ℕ∞
K : Compacts E
i : ℕ
f : 𝓓^{n}_{K}(E, F)
hk : k + 1 ≤ n
⊢ (ContDiffMapSupportedIn.seminorm 𝕜 E (E →L[ℝ] F) k K i) ((fderivLM 𝕜 n k) f) ≤
    (ContDiffMapSupportedIn.seminorm 𝕜 E F n K (i + 1)) f