mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.SmoothApprox

Goal state before:
pp: 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
this✝ : ∀ᶠ (y : M) in 𝓝 x, y ∉ S ∧ dist (f x) (f y) < ε y
this : ∀ᶠ (y : M) in 𝓝 x, (y ∉ S ∧ dist (f x) (f y) < ε y) ∧ (f y = 0 → f x = 0)
y : M
hy : y ∈ {x_1 | (fun y ↦ (y ∉ S ∧ dist (f x) (f y) < ε y) ∧ (f y = 0 → f x = 0)) x_1}
⊢ y ∈ S → (fun x_1 ↦ f x) y = f y

Tactic:
by

Goal state after:
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
s : Set α
f : ↥(Lp E 2 μ)
hs : MeasurableSet s
c : E
hμs : μ s ≠ ∞
x : α
hx : ↑↑(indicatorConstLp 2 hs hμs c) x = s.indicator (fun x ↦ c) x
⊢ ⟪↑↑(indicatorConstLp 2 hs hμs c) x, ↑↑f x⟫ = s.indicator (fun x ↦ ⟪c, ↑↑f x⟫) x

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst✝⁷ : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
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φ : IntegrableOn φ (↑K) μ
f : 𝓓^{n}_{K}(E, F₁)
this : IntegrableOn (fun x ↦ (B (f x)) (φ x)) (↑K) μ
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.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
s : Set α
f : ↥(Lp E 2 μ)
hs : MeasurableSet s
c : E
hμs : μ s ≠ ∞
⊢ ⟪indicatorConstLp 2 hs hμs c, f⟫ = ∫ (x : α) in s, ⟪c, ↑↑f x⟫ ∂μ

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.SmoothApprox

Goal state before:
pp: 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
⊢ ∃ g, (∀ (x : M), dist (g x) (f x) < ε x) ∧ EqOn (⇑g) f S ∧ support ⇑g ⊆ support f

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst✝⁷ : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
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φ : IntegrableOn φ (↑K) μ
f : 𝓓^{n}_{K}(E, F₁)
this : IntegrableOn (fun x ↦ (B (f x)) (φ x)) (↑K) μ
⊢ Integrable (fun x ↦ (B (f x)) (φ x)) μ

Tactic:
by

Goal state after:
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
s : Set α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
f : ↥(Lp E 2 μ)
⊢ ⟪indicatorConstLp 2 hs hμs c, f⟫ = ⟪c, ∫ (x : α) in s, ↑↑f x ∂μ⟫

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.SmoothApprox

Goal state before:
pp: 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
⊢ ∃ g, (∀ (x : M), dist (g x) (f x) < ε x) ∧ support ⇑g ⊆ support f

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: α : Type u_1
𝕜 : Type u_4
inst✝ : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
f : ↥(Lp 𝕜 2 μ)
⊢ ⟪indicatorConstLp 2 hs hμs 1, f⟫ = ∫ (x : α) in s, ↑↑f x ∂μ

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst✝⁷ : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
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φ : IntegrableOn φ (↑K) μ
f : 𝓓^{n}_{K}(E, F₁)
⊢ Integrable (fun x ↦ (B (f x)) (φ x)) μ

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.SmoothApprox

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
ε : E → ℝ
n : ℕ∞
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
ε_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ε
ε_pos : ∀ (x : E), 0 < ε x
S U : Set E
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] S
hU : U ∈ 𝓝ˢ S
hfU : ContDiffOn ℝ (↑n) f U
⊢ ∃ g, ContDiff ℝ (↑n) g ∧ (∀ (x : E), dist (g x) (f x) < ε x) ∧ EqOn g f S ∧ support g ⊆ support f

Tactic:
by

Goal state after:
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
s t : Set α
inst✝ : CompleteSpace E
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ∞
hμt : μ t ≠ ∞
a b : E
⊢ ⟪indicatorConstLp 2 hs hμs a, indicatorConstLp 2 ht hμt b⟫ = μ.real (s ∩ t) • ⟪a, b⟫

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: α : Type u_1
𝕜 : Type u_4
inst✝ : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ∞
hμt : μ t ≠ ∞
⊢ ⟪indicatorConstLp 2 hs hμs 1, indicatorConstLp 2 ht hμt 1⟫ = ↑(μ.real (s ∩ t))

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.SmoothApprox

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
ε : E → ℝ
n : ℕ∞
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
ε_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ε
ε_pos : ∀ (x : E), 0 < ε x
⊢ ∃ g, ContDiff ℝ (↑n) g ∧ (∀ (x : E), dist (g x) (f x) < ε x) ∧ support g ⊆ support f

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ∞
hμt : μ t ≠ ∞
⊢ ⟪indicatorConstLp 2 hs hμs 1, indicatorConstLp 2 ht hμt 1⟫_ℝ = μ.real (s ∩ t)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst✝ : Finite ι
s : ι → Set α
mv : ∀ (j : ι), MeasurableSet (s j)
hv : ∀ (j : ι), μ (s j) ≠ ∞
⊢ (Matrix.of fun i j ↦ μ.real (s i ∩ s j)).PosSemidef

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
inst✝¹ : RCLike 𝕜
μ : Measure α
inst✝ : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
⊢ ⟪(BoundedContinuousFunction.toLp 2 μ 𝕜) f, (BoundedContinuousFunction.toLp 2 μ 𝕜) g⟫ =
    ∫ (x : α), g x * (starRingEnd 𝕜) (f x) ∂μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : RCLike 𝕜
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : CompactSpace α
f g : C(α, 𝕜)
⊢ ⟪(ContinuousMap.toLp 2 μ 𝕜) f, (ContinuousMap.toLp 2 μ 𝕜) g⟫ = ∫ (x : α), g x * (starRingEnd 𝕜) (f x) ∂μ

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst✝¹⁰ : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝⁹ : NormedAddCommGroup F₁
inst✝⁸ : NormedSpace 𝕜 F₁
inst✝⁷ : NormedSpace ℝ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace 𝕜 F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace 𝕜 F₃
inst✝² : SMulCommClass ℝ 𝕜 F₁
inst✝¹ : NormedSpace ℝ F₃
inst✝ : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
f : 𝓓^{n}_{K}(E, F₁)
⊢ (integralAgainstBilinLM B μ φ) f = if IntegrableOn φ (↑K) μ then ∫ (x : E), (B (f x)) (φ x) ∂μ else 0

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst✝¹⁰ : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝⁹ : NormedAddCommGroup F₁
inst✝⁸ : NormedSpace 𝕜 F₁
inst✝⁷ : NormedSpace ℝ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace 𝕜 F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace 𝕜 F₃
inst✝² : SMulCommClass ℝ 𝕜 F₁
inst✝¹ : NormedSpace ℝ F₃
inst✝ : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : IntegrableOn φ (↑K) μ
f : 𝓓^{n}_{K}(E, F₁)
⊢ (integralAgainstBilinLM B μ φ) f = ∫ (x : E), (B (f x)) (φ x) ∂μ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.SmoothApprox

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁷ : MeasurableSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ F
μ : Measure E
inst✝ : IsFiniteMeasureOnCompacts μ
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
⊢ Continuous fun x ↦ ε

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.SmoothApprox

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁷ : MeasurableSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ F
μ : Measure E
inst✝ : IsFiniteMeasureOnCompacts μ
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
⊢ ∀ (x : E), 0 < ε

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst✝¹⁰ : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝⁹ : NormedAddCommGroup F₁
inst✝⁸ : NormedSpace 𝕜 F₁
inst✝⁷ : NormedSpace ℝ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace 𝕜 F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace 𝕜 F₃
inst✝² : SMulCommClass ℝ 𝕜 F₁
inst✝¹ : NormedSpace ℝ F₃
inst✝ : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : IntegrableOn φ (↑K) μ
f : 𝓓^{n}_{K}(E, F₁)
⊢ (integralAgainstBilinLM B μ φ) f = ∫ (x : E) in ↑K, (B (f x)) (φ x) ∂μ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.SmoothApprox

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁷ : MeasurableSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ F
μ : Measure E
inst✝ : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : ¬f =ᵐ[μ] 0
hs₁ : μ (tsupport f) ≠ ∞
⊢ 0 < (μ (tsupport f)).toReal

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ContinuousMapDense

Goal state before:
pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst✝⁶] s
u_open : IsOpen[inst✝⁶] u
hsu : s ⊆ u
hs : μ s ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x ↦ c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen[inst✝⁶] V
h'V : μ V < ∞
hV : μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : μ v < ∞
g : C(α, ℝ)
hgv : EqOn (⇑g) 0 (u ∩ V)ᶜ
hgs : EqOn (⇑g) 1 s
hg_range : ∀ (x : α), g x ∈ Icc 0 1
x : α
⊢ ‖g x‖ = g x

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst✝¹⁰ : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝⁹ : NormedAddCommGroup F₁
inst✝⁸ : NormedSpace 𝕜 F₁
inst✝⁷ : NormedSpace ℝ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace 𝕜 F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace 𝕜 F₃
inst✝² : SMulCommClass ℝ 𝕜 F₁
inst✝¹ : NormedSpace ℝ F₃
inst✝ : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
f : 𝓓^{n}_{K}(E, F₁)
hφ : IntegrableOn φ (↑K) μ
⊢ ∀ᵐ (x : E) ∂μ.restrict ↑K, ‖(B (f x)) (φ x)‖ ≤ ‖φ x‖ * ‖B‖ * (ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0) f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.SmoothApprox

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁷ : MeasurableSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ F
μ : Measure E
inst✝ : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : ¬f =ᵐ[μ] 0
hs₁ : μ (tsupport f) ≠ ∞
hs₂ : 0 < (μ (tsupport f)).toReal
ε' : ℝ := ε * (μ (tsupport f)).toReal ^ (-(1 / p.toReal))
ε'_def : ε' = ε * (μ (tsupport f)).toReal ^ (-(1 / p.toReal))
⊢ 0 < ε'

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.ContinuousMapDense

Goal state before:
pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst✝⁶] s
u_open : IsOpen[inst✝⁶] u
hsu : s ⊆ u
hs : μ s ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x ↦ c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen[inst✝⁶] V
h'V : μ V < ∞
hV : μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : μ v < ∞
g : C(α, ℝ)
hgv : EqOn (⇑g) 0 (u ∩ V)ᶜ
hgs : EqOn (⇑g) 1 s
hg_range : ∀ (x : α), g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖g x‖ = g x
⊢ ∀ (x : α), ‖g x • c‖ ≤ ‖c‖

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst✝¹⁰ : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝⁹ : NormedAddCommGroup F₁
inst✝⁸ : NormedSpace 𝕜 F₁
inst✝⁷ : NormedSpace ℝ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace 𝕜 F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace 𝕜 F₃
inst✝² : SMulCommClass ℝ 𝕜 F₁
inst✝¹ : NormedSpace ℝ F₃
inst✝ : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
f : 𝓓^{n}_{K}(E, F₁)
⊢ ‖(integralAgainstBilinLM B μ φ) f‖ ≤
    (∫ (x : E) in ↑K, ‖φ x‖ ∂μ) * ‖B‖ * (ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0) f

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝²¹ : NontriviallyNormedField 𝕜
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
inst✝¹⁸ : NormedAddCommGroup F
inst✝¹⁷ : NormedSpace ℝ F
inst✝¹⁶ : NormedSpace 𝕜 F
inst✝¹⁵ : SMulCommClass ℝ 𝕜 F
inst✝¹⁴ : NormedAddCommGroup F'
inst✝¹³ : NormedSpace ℝ F'
inst✝¹² : NormedSpace 𝕜 F'
inst✝¹¹ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
m : MeasurableSpace E
inst✝¹⁰ : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝⁹ : NormedAddCommGroup F₁
inst✝⁸ : NormedSpace 𝕜 F₁
inst✝⁷ : NormedSpace ℝ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace 𝕜 F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace 𝕜 F₃
inst✝² : SMulCommClass ℝ 𝕜 F₁
inst✝¹ : NormedSpace ℝ F₃
inst✝ : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
⊢ 0 ≤ (∫ (x : E) in ↑K, ‖φ x‖ ∂μ) * ‖B‖

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝²¹ : NontriviallyNormedField 𝕜
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
inst✝¹⁸ : NormedAddCommGroup F
inst✝¹⁷ : NormedSpace ℝ F
inst✝¹⁶ : NormedSpace 𝕜 F
inst✝¹⁵ : SMulCommClass ℝ 𝕜 F
inst✝¹⁴ : NormedAddCommGroup F'
inst✝¹³ : NormedSpace ℝ F'
inst✝¹² : NormedSpace 𝕜 F'
inst✝¹¹ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
m : MeasurableSpace E
inst✝¹⁰ : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝⁹ : NormedAddCommGroup F₁
inst✝⁸ : NormedSpace 𝕜 F₁
inst✝⁷ : NormedSpace ℝ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace 𝕜 F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace 𝕜 F₃
inst✝² : SMulCommClass ℝ 𝕜 F₁
inst✝¹ : NormedSpace ℝ F₃
inst✝ : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
f : 𝓓^{n}_{K}(E, F₁)
⊢ ‖(integralAgainstBilinLM B μ φ) f‖ ≤
    (∫ (x : E) in ↑K, ‖φ x‖ ∂μ) * ‖B‖ * ({0}.sup fun i ↦ ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K i) f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.SmoothApprox

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁷ : MeasurableSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ F
μ : Measure E
inst✝ : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : ¬f =ᵐ[μ] 0
hs₁ : μ (tsupport f) ≠ ∞
hs₂ : 0 < (μ (tsupport f)).toReal
ε' : ℝ := ε * (μ (tsupport f)).toReal ^ (-(1 / p.toReal))
ε'_def : ε' = ε * (μ (tsupport f)).toReal ^ (-(1 / p.toReal))
hε' : 0 < ε'
⊢ ENNReal.ofReal ε' * μ (tsupport f) ^ (1 / p.toReal) ≤ ENNReal.ofReal ε

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.SmoothApprox

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁷ : MeasurableSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ F
μ : Measure E
inst✝ : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : ¬f =ᵐ[μ] 0
hs₁ : μ (tsupport f) ≠ ∞
hs₂ : 0 < (μ (tsupport f)).toReal
ε' : ℝ := ε * (μ (tsupport f)).toReal ^ (-(1 / p.toReal))
ε'_def : ε' = ε * (μ (tsupport f)).toReal ^ (-(1 / p.toReal))
hε' : 0 < ε'
hε₂ : ENNReal.ofReal ε' * μ (tsupport f) ^ (1 / p.toReal) ≤ ENNReal.ofReal ε
⊢ Continuous fun x ↦ ε'

Tactic:
by

Goal state after: