mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Lp.SmoothApprox

Goal state before:
pp: case inl
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
g : E → F
hg₁ : ContDiff ℝ ∞ g
hg₂ : ∀ (x : E), dist (g x) (f x) < ε
hg₃ : Function.support g ⊆ Function.support f
x : E
⊢ ‖(f - g) x‖ ≤ ε

Tactic:
simpa using

Goal state after:
case inl
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
g : E → F
hg₁ : ContDiff ℝ ∞ g
hg₂ : ∀ (x : E), dist (g x) (f x) < ε
hg₃ : Function.support g ⊆ Function.support f
x : E
⊢ dist (g x) (f x) ≤ ε
Module: Mathlib.MeasureTheory.Function.ContinuousMapDense

Goal state before:
pp: case pos.inl
α : 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
gc_bd0 : ∀ (x : α), ‖g x • c‖ ≤ ‖c‖
x : α
hsv : x ∈ v \ s
⊢ ‖g x • c - s.indicator (fun _x ↦ c) x‖ ≤ ‖(v \ s).indicator (fun _x ↦ c) x‖

Tactic:
simpa using

Goal state after:
case pos.inl
α : 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
gc_bd0 : ∀ (x : α), ‖g x • c‖ ≤ ‖c‖
x : α
hsv : x ∈ v \ s
⊢ ‖g x • c‖ ≤ ‖c‖
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∞
hp : p ≠ ∞
hp₂ : Fact (1 ≤ p)
f : ↥(Lp F p μ)
⊢ f ∈ closure {f | ∃ g, ↑↑f =ᵐ[μ] g ∧ HasCompactSupport g ∧ ContDiff ℝ ∞ g}

Tactic:
refine (mem_closure_iff_nhds_basis Metric.nhds_basis_closedBall).2 fun ε hε ↦ ?_

Goal state after:
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∞
hp : p ≠ ∞
hp₂ : Fact (1 ≤ p)
f : ↥(Lp F p μ)
ε : ℝ
hε : 0 < ε
⊢ ∃ y ∈ {f | ∃ g, ↑↑f =ᵐ[μ] g ∧ HasCompactSupport g ∧ ContDiff ℝ ∞ g}, y ∈ Metric.closedBall f ε
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
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
G : Type u_8
inst✝⁹ : NormedAlgebra ℝ 𝕜
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace 𝕜 F₁
inst✝⁶ : NormedSpace ℝ F₁
inst✝⁵ : NormedAddCommGroup F₂
inst✝⁴ : NormedSpace 𝕜 F₂
inst✝³ : NormedSpace ℝ F₂
inst✝² : NormedAddCommGroup F₃
inst✝¹ : NormedSpace 𝕜 F₃
inst✝ : NormedSpace ℝ F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
g : E → F₂
hg : ContDiff ℝ (↑n) g
k : ℕ
hk : ↑k ≤ n
hcont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun x ↦
    (Finset.range (k + 1)).sup' ⋯ fun i ↦ ‖iteratedFDeriv ℝ i g x‖
C₀ : ℝ
hC₀ : ∀ x ∈ ↑K, ‖(Finset.range (k + 1)).sup' ⋯ fun i ↦ ‖iteratedFDeriv ℝ i g x‖‖ ≤ C₀
hgC₀ : ∀ i ≤ k, ∀ x ∈ K, ‖iteratedFDeriv ℝ i g x‖ ≤ ‖C₀‖
φ : 𝓓^{n}_{K}(E, F₁)
x : E
hx : x ∈ K
⊢ ‖iteratedFDeriv ℝ k (fun y ↦ (B (φ y)) (g y)) x‖ ≤
    ‖B‖ * ∑ i ∈ Finset.range (k + 1), ↑(k.choose i) * ‖iteratedFDeriv ℝ i (⇑φ) x‖ * ‖iteratedFDeriv ℝ (k - i) g x‖

Tactic:
simpa using

Goal state after:
𝕜 : 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
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
G : Type u_8
inst✝⁹ : NormedAlgebra ℝ 𝕜
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace 𝕜 F₁
inst✝⁶ : NormedSpace ℝ F₁
inst✝⁵ : NormedAddCommGroup F₂
inst✝⁴ : NormedSpace 𝕜 F₂
inst✝³ : NormedSpace ℝ F₂
inst✝² : NormedAddCommGroup F₃
inst✝¹ : NormedSpace 𝕜 F₃
inst✝ : NormedSpace ℝ F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
g : E → F₂
hg : ContDiff ℝ (↑n) g
k : ℕ
hk : ↑k ≤ n
hcont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun x ↦
    (Finset.range (k + 1)).sup' ⋯ fun i ↦ ‖iteratedFDeriv ℝ i g x‖
C₀ : ℝ
hC₀ : ∀ x ∈ ↑K, ‖(Finset.range (k + 1)).sup' ⋯ fun i ↦ ‖iteratedFDeriv ℝ i g x‖‖ ≤ C₀
hgC₀ : ∀ i ≤ k, ∀ x ∈ K, ‖iteratedFDeriv ℝ i g x‖ ≤ ‖C₀‖
φ : 𝓓^{n}_{K}(E, F₁)
x : E
hx : x ∈ K
⊢ ‖iteratedFDeriv ℝ k (fun y ↦ (B (φ y)) (g y)) x‖ ≤
    ‖B‖ * ∑ i ∈ Finset.range (k + 1), ↑(k.choose i) * ‖iteratedFDeriv ℝ i (⇑φ) x‖ * ‖iteratedFDeriv ℝ (k - i) g x‖
Module: Mathlib.Analysis.Normed.Module.Bases

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
β : Type u_3
L : SummationFilter β
b : GeneralSchauderBasis β 𝕜 X L
l : β →₀ 𝕜
hl : (Finsupp.linearCombination 𝕜 ↑b) l = 0
⊢ ∀ (a : β), l a = 0 a

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
β : Type u_3
L : SummationFilter β
b : GeneralSchauderBasis β 𝕜 X L
l : β →₀ 𝕜
hl : (Finsupp.linearCombination 𝕜 ↑b) l = 0
⊢ ∀ (a : β), l a = 0
Module: Mathlib.Analysis.Normed.Module.Bases

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
β : Type u_3
b : UnconditionalSchauderBasis β 𝕜 X
inst✝ : CompleteSpace X
C : ℝ
hC : ∀ (A : Finset β), ‖GeneralSchauderBasis.proj b A‖ ≤ C
⊢ 0 ≤ C

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
β : Type u_3
b : UnconditionalSchauderBasis β 𝕜 X
inst✝ : CompleteSpace X
C : ℝ
hC : ∀ (A : Finset β), ‖GeneralSchauderBasis.proj b A‖ ≤ C
⊢ 0 ≤ C
Module: Mathlib.Analysis.Normed.Module.Bases

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
b : SchauderBasis 𝕜 X
inst✝ : CompleteSpace X
C : ℝ
hC : ∀ (n : ℕ), ‖b.proj n‖ ≤ C
⊢ 0 ≤ C

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
b : SchauderBasis 𝕜 X
inst✝ : CompleteSpace X
C : ℝ
hC : ∀ (n : ℕ), ‖b.proj n‖ ≤ C
⊢ 0 ≤ C
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 α
inst✝³ : NormedSpace ℝ E
inst✝² : R1Space α
inst✝¹ : WeaklyLocallyCompactSpace α
inst✝ : μ.Regular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
⊢ ENNReal.ofReal p ≠ 0

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝⁸ : TopologicalSpace α
inst✝⁷ : NormalSpace α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : BorelSpace α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
μ : Measure α
inst✝³ : NormedSpace ℝ E
inst✝² : R1Space α
inst✝¹ : WeaklyLocallyCompactSpace α
inst✝ : μ.Regular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
⊢ 0 < p
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv

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
V : Type u_7
F : Type u_8
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedSpace ℝ E
inst✝¹ : RCLike 𝕜
inst✝ : NormedSpace 𝕜 F
x✝ : ℕ × ℕ
k n : ℕ
f : 𝓢(ℝ, F)
x : ℝ
⊢ ‖x‖ ^ (k, n).1 * ‖iteratedFDeriv ℝ (k, n).2 (deriv ⇑f) x‖ ≤ 1 * ({(k, n + 1)}.sup (schwartzSeminormFamily 𝕜 ℝ F)) f

Tactic:
simpa using

Goal state after:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F✝ : Type u_6
V : Type u_7
F : Type u_8
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedSpace ℝ E
inst✝¹ : RCLike 𝕜
inst✝ : NormedSpace 𝕜 F
x✝ : ℕ × ℕ
k n : ℕ
f : 𝓢(ℝ, F)
x : ℝ
⊢ |x| ^ k * ‖iteratedDeriv (n + 1) (⇑f) x‖ ≤ (SchwartzMap.seminorm 𝕜 k (n + 1)) f
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv

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
V : Type u_7
F : Type u_8
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedSpace ℝ E
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
x✝ : ℕ × ℕ
k n : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ (k, n).1 * ‖iteratedFDeriv ℝ (k, n).2 (fderiv ℝ ⇑f) x‖ ≤ 1 * ({(k, n + 1)}.sup (schwartzSeminormFamily 𝕜 E F)) f

Tactic:
simpa using

Goal state after:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F✝ : Type u_6
V : Type u_7
F : Type u_8
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedSpace ℝ E
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
x✝ : ℕ × ℕ
k n : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ (n + 1) (⇑f) x‖ ≤ (SchwartzMap.seminorm 𝕜 k (n + 1)) f
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 α
inst✝³ : NormedSpace ℝ E
inst✝² : R1Space α
inst✝¹ : WeaklyLocallyCompactSpace α
inst✝ : μ.Regular
f : α → E
ε : ℝ
hε : 0 < ε
hf : MemLp f (ENNReal.ofReal 1) μ
⊢ ∃ g,
    HasCompactSupport g ∧
      ∫ (x : α), ‖f x - g x‖ ∂μ ≤ ε ∧
        Continuous[inst✝⁸, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g (ENNReal.ofReal 1) μ

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝⁸ : TopologicalSpace α
inst✝⁷ : NormalSpace α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : BorelSpace α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
μ : Measure α
inst✝³ : NormedSpace ℝ E
inst✝² : R1Space α
inst✝¹ : WeaklyLocallyCompactSpace α
inst✝ : μ.Regular
f : α → E
ε : ℝ
hε : 0 < ε
hf : MemLp f (ENNReal.ofReal 1) μ
⊢ ∃ g,
    HasCompactSupport g ∧
      ∫ (x : α), ‖f x - g x‖ ∂μ ≤ ε ∧
        Continuous[inst✝⁸, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g 1 μ
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 α
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.WeaklyRegular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
⊢ ENNReal.ofReal p ≠ 0

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.WeaklyRegular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
A : ENNReal.ofReal (ε ^ (1 / p)) ≠ 0
⊢ 0 < p
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 α
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.WeaklyRegular
f : α → E
ε : ℝ
hε : 0 < ε
hf : MemLp f (ENNReal.ofReal 1) μ
⊢ ∃ g, ∫ (x : α), ‖f x - g x‖ ∂μ ≤ ε ∧ MemLp (⇑g) (ENNReal.ofReal 1) μ

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.WeaklyRegular
f : α → E
ε : ℝ
hε : 0 < ε
hf : MemLp f (ENNReal.ofReal 1) μ
⊢ ∃ g, ∫ (x : α), ‖f x - g x‖ ∂μ ≤ ε ∧ MemLp (⇑g) 1 μ
Module: Mathlib.Analysis.InnerProductSpace.l2Space

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : DecidableEq ι
i : ι
a : G i
f : ↥(lp G 2)
⊢ ⟪f, lp.single 2 i a⟫ = ⟪↑f i, a⟫

Tactic:
simpa using

Goal state after:
ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : DecidableEq ι
i : ι
a : G i
f : ↥(lp G 2)
⊢ ⟪f, lp.single 2 i a⟫ = ⟪↑f i, a⟫
Module: Mathlib.Analysis.InnerProductSpace.l2Space

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
inst✝⁶ : RCLike 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (G i)
inst✝² : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝¹ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : DecidableEq ι
i : ι
x : G i
⊢ hV.linearIsometry (lp.single 2 i x) = (V i) x

Tactic:
rw [hV.linearIsometry_apply, ← tsum_ite_eq i (fun _ ↦ V i x)]
  congr
  ext j
  rw [lp.single_apply]
  split_ifs with h
  · subst h; simp
  · simp [h]

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

Goal state before:
pp: T : ℝ
m n : ℤ
x : AddCircle T
⊢ ↑((m + n) • x).toCircle = (fourier m) x * (fourier n) x

Tactic:
rw [← fourier_apply]; exact fourier_add

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

Goal state before:
pp: case refine_2
ι : Type u_1
𝕜 : Type u_2
inst✝⁶ : RCLike 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (G i)
inst✝² : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝¹ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
⊢ (⨆ i, (V i).range).topologicalClosure ≤ hV.linearIsometry.range

Tactic:
apply topologicalClosure_minimal
    · refine iSup_le ?_
      rintro i x ⟨x, rfl⟩
      use lp.single 2 i x
      exact hV.linearIsometry_apply_single x
    exact hV.linearIsometry.isometry.isUniformInducing.isComplete_range.isClosed

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : CompleteSpace E
F : ι → Submodule 𝕜 E
inst✝ : ∀ (i : ι), CompleteSpace ↥(F i)
hFortho : OrthogonalFamily 𝕜 (fun i ↦ ↥(F i)) fun i ↦ (F i).subtypeₗᵢ
hFtotal : ⊤ ≤ (⨆ i, F i).topologicalClosure
⊢ ⊤ ≤ (⨆ i, (F i).subtypeₗᵢ.range).topologicalClosure

Tactic:
simpa using

Goal state after:
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : CompleteSpace E
F : ι → Submodule 𝕜 E
inst✝ : ∀ (i : ι), CompleteSpace ↥(F i)
hFortho : OrthogonalFamily 𝕜 (fun i ↦ ↥(F i)) fun i ↦ (F i).subtypeₗᵢ
hFtotal : ⊤ ≤ (⨆ i, F i).topologicalClosure
⊢ (⨆ i, F i).topologicalClosure = ⊤
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: case e'_9
T : ℝ
hT : Fact (0 < T)
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
e_3✝ : Complex.instSemiring = NormedField.toNormedCommRing.toSemiring
e_6✝ : Lp.instModule ≍ Lp.instModule
⊢ span ℂ (⇑(toLp p haarAddCircle ℂ) '' range fourier) = span ℂ (⇑↑(toLp p haarAddCircle ℂ) '' range fourier)

Tactic:
simp only [ContinuousLinearMap.coe_coe]

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
i j : ℤ
⊢ inner ℂ (fourierLp 2 i) (fourierLp 2 j) = if i = j then 1 else 0

Tactic:
ContinuousMap.inner_toLp (@haarAddCircle T hT) (fourier i) (fourier j)

Goal state after:
T : ℝ
hT : Fact (0 < T)
i j : ℤ
⊢ ∫ (x : AddCircle T), (fourier j) x * (starRingEnd ℂ) ((fourier i) x) ∂haarAddCircle = if i = j then 1 else 0
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : AddCircle T → E
hf : Integrable f haarAddCircle
hg : Integrable g haarAddCircle
x : ℤ
⊢ fourierCoeff (f + g) x = (fourierCoeff f + fourierCoeff g) x

Tactic:
simpa using

Goal state after:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : AddCircle T → E
hf : Integrable f haarAddCircle
hg : Integrable g haarAddCircle
x : ℤ
⊢ ∫ (t : AddCircle T), (fourier (-x)) t • f t + (fourier (-x)) t • g t ∂haarAddCircle =
    ∫ (t : AddCircle T), (fourier (-x)) t • f t ∂haarAddCircle +
      ∫ (t : AddCircle T), (fourier (-x)) t • g t ∂haarAddCircle
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
ι : Type u_2
f : ι → AddCircle T → E
a : ι
s : Finset ι
ha : a ∉ s
iha : (∀ i ∈ s, Integrable (f i) haarAddCircle) → fourierCoeff (∑ i ∈ s, f i) = ∑ i ∈ s, fourierCoeff (f i)
hf : ∀ i ∈ insert a s, Integrable (f i) haarAddCircle
⊢ ?m.70

Tactic:
simpa using

Goal state after:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
ι : Type u_2
f : ι → AddCircle T → E
a : ι
s : Finset ι
ha : a ∉ s
iha : (∀ i ∈ s, Integrable (f i) haarAddCircle) → fourierCoeff (∑ i ∈ s, f i) = ∑ i ∈ s, fourierCoeff (f i)
hf : ∀ i ∈ insert a s, Integrable (f i) haarAddCircle
⊢ ?m.70
Module: Mathlib.Analysis.InnerProductSpace.l2Space

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x : E
⊢ HasSum (fun i ↦ ↑(b.repr x) i • b i) x

Tactic:
simpa using

Goal state after:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x : E
⊢ HasSum (fun i ↦ ↑(b.repr x) i • b i) x
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
ι : Type u_2
s : Finset ι
f : ι → AddCircle T → E
hf : ∀ i ∈ s, Integrable (f i) haarAddCircle
⊢ fourierCoeff (∑ i ∈ s, f i) = ∑ i ∈ s, fourierCoeff (f i)

Tactic:
by
  classical
  induction s using Finset.induction_on with
  | empty => ext; simp [fourierCoeff]
  | insert a s ha iha =>
      obtain ⟨hf₁, hf₂⟩ := by simpa using hf
      rw [s.sum_insert ha, s.sum_insert ha,
        fourierCoeff.add hf₁ (integrable_finsetSum' s hf₂), iha hf₂]

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : Fintype ι
b : HilbertBasis ι 𝕜 E
this : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑(span 𝕜 ↑(Finset.image (⇑b) Finset.univ))
⊢ span 𝕜 (Set.range ⇑b) = ⊤

Tactic:
simpa using

Goal state after:
ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : Fintype ι
b : HilbertBasis ι 𝕜 E
this : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑(span 𝕜 ↑(Finset.image (⇑b) Finset.univ))
⊢ span 𝕜 (Set.range ⇑b) = ⊤
Module: Mathlib.Analysis.InnerProductSpace.l2Space

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
i j : ι
⊢ ((innerSL 𝕜) (b i)) (b j) = Pi.single j 1 i

Tactic:
simpa using

Goal state after:
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
i j : ι
⊢ ⟪b i, b j⟫ = if i = j then 1 else 0
Module: Mathlib.Analysis.InnerProductSpace.l2Space

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
x : E
⊢ HasSum (fun i ↦ ((innerSL 𝕜) (b i)) x • b i) x

Tactic:
simpa using

Goal state after:
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
x : E
⊢ HasSum (fun i ↦ ↑(b.repr x) i • b i) x
Module: Mathlib.Analysis.InnerProductSpace.l2Space

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
inst✝ : CompleteSpace ↥U
b : HilbertBasis ι 𝕜 ↥U
x : E
⊢ HasSum (fun i ↦ ⟪↑(b i), x⟫ • b i) (U.orthogonalProjectionOnto x)

Tactic:
simpa using

Goal state after:
ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
inst✝ : CompleteSpace ↥U
b : HilbertBasis ι 𝕜 ↥U
x : E
⊢ HasSum (fun i ↦ ⟪↑(b i), x⟫ • b i) (U.orthogonalProjectionOnto x)