mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv

Goal state before:
pp: E : Type u_5
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : FiniteDimensional ℝ E
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace ℝ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace ℝ F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace ℝ F₃
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
L : F₁ →L[ℝ] F₂ →L[ℝ] F₃
⊢ ∫ (x : E), (L (f x)) ((Δ g) x) ∂μ = ∫ (x : E), (L ((Δ f) x)) (g x) ∂μ

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✝ : μ.WeaklyRegular
hp : p ≠ ∞
f : α → E
hf : MemLp f p μ
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : μ t < ∞
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ δ → eLpNorm g p μ ≤ δ → eLpNorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x ↦ c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_closed : IsClosed[inst✝⁶] s
μs : μ (t \ s) < ↑η
hsμ : μ s < ∞
⊢ eLpNorm ((s.indicator fun _y ↦ c) - t.indicator fun _y ↦ c) p μ ≤ δ

Tactic:
by

Goal state after:
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
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank 𝕜 ↥(↑(P n)).range = n
hcomp : ∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x
n : ℕ
U : Submodule 𝕜 X := (↑(succSub P n)).range
V : Submodule 𝕜 X := (↑(P n)).range
W : Submodule 𝕜 X := (↑(P (n + 1))).range
hV : V ≤ W
hUW : U ≤ W
hW : W = U ⊔ V
x : X
x✝ : x ∈ U ⊓ V
y : X
hy : ↑(succSub P n) y = x
z : X
hz : ↑(P n) z = x
⊢ x = (P n) x

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✝ : μ.WeaklyRegular
hp : p ≠ ∞
f✝ : α → E
hf : MemLp f✝ p μ
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : μ t < ∞
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ δ → eLpNorm g p μ ≤ δ → eLpNorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x ↦ c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_closed : IsClosed[inst✝⁶] s
μs : μ (t \ s) < ↑η
hsμ : μ s < ∞
I1 : eLpNorm ((s.indicator fun _y ↦ c) - t.indicator fun _y ↦ c) p μ ≤ δ
f : α → E
f_cont : Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
I2 : eLpNorm (fun x ↦ f x - s.indicator (fun _y ↦ c) x) p μ ≤ δ
f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖
f_mem : MemLp f p μ
⊢ eLpNorm (f - t.indicator fun _y ↦ c) p μ ≤ ε

Tactic:
by

Goal state after:
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
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank 𝕜 ↥(↑(P n)).range = n
hcomp : ∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x
n : ℕ
U : Submodule 𝕜 X := (↑(succSub P n)).range
V : Submodule 𝕜 X := (↑(P n)).range
W : Submodule 𝕜 X := (↑(P (n + 1))).range
hV : V ≤ W
hUW : U ≤ W
hW : W = U ⊔ V
x : X
x✝ : x ∈ U ⊓ V
y : X
hy : ↑(succSub P n) y = x
z : X
hz : ↑(P n) z = x
⊢ (P n) x = 0

Tactic:
by

Goal state after:
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
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank 𝕜 ↥(↑(P n)).range = n
hcomp : ∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x
n : ℕ
U : Submodule 𝕜 X := (↑(succSub P n)).range
V : Submodule 𝕜 X := (↑(P n)).range
W : Submodule 𝕜 X := (↑(P (n + 1))).range
hV : V ≤ W
hUW : U ≤ W
hW : W = U ⊔ V
x : X
x✝ : x ∈ U ⊓ V
y : X
hy : ↑(succSub P n) y = x
z : X
hz : ↑(P n) z = x
⊢ x ∈ ⊥

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✝ : μ.WeaklyRegular
hp : p ≠ ∞
f : α → E
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ g, eLpNorm (f - ⇑g) p μ ≤ ε ∧ MemLp (⇑g) p μ

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 α
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.WeaklyRegular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
I : 0 < ε ^ (1 / p)
⊢ ENNReal.ofReal (ε ^ (1 / p)) ≠ 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 α
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:
by

Goal state after:
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
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank 𝕜 ↥(↑(P n)).range = n
hcomp : ∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x
n : ℕ
U : Submodule 𝕜 X := (↑(succSub P n)).range
V : Submodule 𝕜 X := (↑(P n)).range
W : Submodule 𝕜 X := (↑(P (n + 1))).range
hV : V ≤ W
hUW : U ≤ W
hW : W = U ⊔ V
hdisj : U ⊓ V = ⊥
⊢ 0 < Module.finrank 𝕜 ↥W

Tactic:
by

Goal state after:
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)
f g : ↥(lp G 2)
⊢ Summable fun i ↦ ⟪↑f i, ↑g i⟫

Tactic:
by

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)
f : ↥(lp G 2)
⊢ ‖f‖ ^ 2 = ‖f‖ ^ ENNReal.toReal 2

Tactic:
by

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)
f : ↥(lp G 2)
⊢ ∑' (i : ι), ‖↑f i‖ ^ ENNReal.toReal 2 = ∑' (i : ι), ‖↑f i‖ ^ 2

Tactic:
by

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)
f : ↥(lp G 2)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

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)
f g : ↥(lp G 2)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

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 α
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.WeaklyRegular
p : ℝ
hp : 0 < p
f : α → E
hf : MemLp f (ENNReal.ofReal p) μ
ε : ℝ
hε : 0 < ε
⊢ ∃ g, ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε ∧ MemLp (⇑g) (ENNReal.ofReal p) μ

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 α
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.WeaklyRegular
f : α → E
hf : Integrable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ g, ∫⁻ (x : α), ‖f x - g x‖ₑ ∂μ ≤ ε ∧ Integrable (⇑g) μ

Tactic:
by

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)
f₁ f₂ g : ↥(lp G 2)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

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 α
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.WeaklyRegular
f : α → E
hf : Integrable f μ
ε : ℝ
hε : 0 < ε
⊢ ∃ g, ∫ (x : α), ‖f x - g x‖ ∂μ ≤ ε ∧ Integrable (⇑g) μ

Tactic:
by

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)
f g : ↥(lp G 2)
c : 𝕜
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

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✝² : SecondCountableTopologyEither α E
inst✝¹ : Fact (1 ≤ p)
hp : p ≠ ∞
inst✝ : μ.WeaklyRegular
⊢ Dense ↑(boundedContinuousFunction E p μ)

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✝⁶ : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
𝕜 : Type u_3
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : IsBoundedSMul 𝕜 E
inst✝² : NormedSpace ℝ E
inst✝¹ : μ.WeaklyRegular
inst✝ : IsFiniteMeasure μ
hp : p ≠ ∞
⊢ DenseRange ⇑(toLp p μ 𝕜)

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✝⁷ : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
𝕜 : Type u_3
inst✝⁶ : NormedRing 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsBoundedSMul 𝕜 E
inst✝³ : NormedSpace ℝ E
inst✝² : CompactSpace α
inst✝¹ : μ.WeaklyRegular
inst✝ : IsFiniteMeasure μ
hp : p ≠ ∞
⊢ DenseRange ⇑(toLp p μ 𝕜)

Tactic:
by

Goal state after:
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
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank 𝕜 ↥(↑(P n)).range = n
hcomp : ∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x
n : ℕ
⊢ Module.finrank 𝕜 ↥(↑(succSub P n)).range = 1

Tactic:
by

Goal state after:
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 : AddCircle T → E
⊢ ∫ (t : AddCircle T), f t ∂haarAddCircle = T⁻¹ • ∫ (t : AddCircle T), f t

Tactic:
by

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
f : AddCircle T → ℂ
p : ℝ≥0∞
hT' : 0 < T
h : MemLp f p AddCircle.haarAddCircle
⊢ ENNReal.ofReal T ≠ ∞

Tactic:
by

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
f : AddCircle T → ℂ
p : ℝ≥0∞
hT' : 0 < T
h : MemLp f p (ENNReal.ofReal T • AddCircle.haarAddCircle)
⊢ (ENNReal.ofReal T)⁻¹ ≠ ∞

Tactic:
by

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
f : AddCircle T → ℂ
p : ℝ≥0∞
hT' : 0 < T
h : MemLp f p (ENNReal.ofReal T • AddCircle.haarAddCircle)
this : MemLp f p (((ENNReal.ofReal T)⁻¹ * ENNReal.ofReal T) • AddCircle.haarAddCircle)
⊢ ENNReal.ofReal T ≠ 0

Tactic:
by

Goal state after:
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
D : RankOneDecomposition 𝕜 X
n : ℕ
x : X
S : X →ₗ[𝕜] X := ↑(succSub D.P n)
hrank : Module.finrank 𝕜 ↥S.range = 1
this : FiniteDimensional 𝕜 ↥S.range
⊢ 𝕜 ∙ D.e n = S.range

Tactic:
by

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
f : AddCircle T → ℂ
p : ℝ≥0∞
hT' : 0 < T
h : MemLp f p (ENNReal.ofReal T • AddCircle.haarAddCircle)
this : MemLp f p (((ENNReal.ofReal T)⁻¹ * ENNReal.ofReal T) • AddCircle.haarAddCircle)
⊢ ENNReal.ofReal T ≠ ∞

Tactic:
by

Goal state after:
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)
⊢ ⟪lp.single 2 i a, f⟫ = ⟪a, ↑f i⟫

Tactic:
by

Goal state after:
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
D : RankOneDecomposition 𝕜 X
n : ℕ
x : X
⊢ ∃ c, c • D.e n = (succSub D.P n) x

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
f : AddCircle T → ℂ
p : ℝ≥0∞
⊢ MemLp f p AddCircle.haarAddCircle ↔ MemLp f p volume

Tactic:
by

Goal state after:
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 : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : ℕ → X → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n) x = coeff n x • D.e n
n : ℕ
x y : X
⊢ (fun x ↦ x • D.e n) (coeff n (x + y)) = (fun x ↦ x • D.e n) (coeff n x + coeff n y)

Tactic:
by

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✝ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
f : ↥(lp G 2)
⊢ Summable fun i ↦ (V i) (↑f i)

Tactic:
by

Goal state after:
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 : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : ℕ → X → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n) x = coeff n x • D.e n
n : ℕ
c : 𝕜
x : X
⊢ (fun x ↦ x • D.e n) (coeff n (c • x)) = (fun x ↦ x • D.e n) ((RingHom.id 𝕜) c • coeff n x)

Tactic:
by

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✝ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV✝ hV : OrthogonalFamily 𝕜 G V
f g : ↥(lp G 2)
⊢ ∑' (i : ι), (V i) (↑(f + g) i) = ∑' (i : ι), (V i) (↑f i) + ∑' (i : ι), (V i) (↑g i)

Tactic:
by

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✝ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV✝ hV : OrthogonalFamily 𝕜 G V
c : 𝕜
f : ↥(lp G 2)
⊢ ∑' (i : ι), (V i) (↑(c • f) i) = (RingHom.id 𝕜) c • ∑' (i : ι), (V i) (↑f i)

Tactic:
by

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

Goal state before:
pp: T : ℝ
n : ℤ
x : ℝ
⊢ (fourier n) ↑x = Complex.exp (2 * ↑π * Complex.I * ↑n * ↑x / ↑T)

Tactic:
by

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✝ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV✝ hV : OrthogonalFamily 𝕜 G V
f : ↥(lp G 2)
⊢ 0 < ENNReal.toReal 2

Tactic:
by

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

Goal state before:
pp: T : ℝ
n : ℤ
x : ℝ
⊢ ↑(toCircle (n • ↑x)) = Complex.exp (2 * ↑π * Complex.I * ↑n * ↑x / ↑T)

Tactic:
by

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

Goal state before:
pp: T : ℝ
x : AddCircle T
⊢ (fourier 0) x = 1

Tactic:
by

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✝ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV✝ hV : OrthogonalFamily 𝕜 G V
f : ↥(lp G 2)
H : 0 < ENNReal.toReal 2
this : ‖∑' (i : ι), (V i) (↑f i)‖ ^ ENNReal.toReal 2 = ‖f‖ ^ ENNReal.toReal 2
⊢ ‖{ toFun := fun f ↦ ∑' (i : ι), (V i) (↑f i), map_add' := ⋯, map_smul' := ⋯ } f‖ = ‖f‖

Tactic:
by

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

Goal state before:
pp: T : ℝ
⊢ ↑(toCircle 0) = 1

Tactic:
by

Goal state after:
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 : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : ℕ → X → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n) x = coeff n x • D.e n
n : ℕ
x : X
⊢ ‖coeff n x • D.e n‖ = ‖(succSub D.P n) x‖

Tactic:
by

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

Goal state before:
pp: T : ℝ
n : ℤ
⊢ (fourier n) 0 = 1

Tactic:
by

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

Goal state before:
pp: T : ℝ
x : AddCircle T
⊢ (fourier 1) x = ↑x.toCircle

Tactic:
by

Goal state after:
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 : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : ℕ → X → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n) x = coeff n x • D.e n
n : ℕ
x : X
⊢ ‖{ toFun := coeff n, map_add' := ⋯, map_smul' := ⋯ } x‖ ≤ ‖succSub D.P n‖ / ‖D.e n‖ * ‖x‖

Tactic:
by

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✝ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV✝ hV : OrthogonalFamily 𝕜 G V
f : ↥(lp G 2)
⊢ ‖{ toFun := fun f ↦ ∑' (i : ι), (V i) (↑f i), map_add' := ⋯, map_smul' := ⋯ } f‖ = ‖f‖

Tactic:
by

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

Goal state before:
pp: T : ℝ
n : ℤ
x : AddCircle T
⊢ (fourier (-n)) x = (starRingEnd ℂ) ((fourier n) x)

Tactic:
by

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

Goal state before:
pp: T : ℝ
n : ℤ
x : AddCircle T
⊢ ↑(-(n • x)).toCircle = (starRingEnd ℂ) ((fourier n) x)

Tactic:
by

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✝¹ : 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:
by

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

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

Tactic:
by

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✝² : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
W₀ : Π₀ (i : ι), G i
⊢ hV.linearIsometry (W₀.sum (lp.single 2)) = W₀.sum fun i ↦ ⇑(V i)

Tactic:
by

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:
by

Goal state after:
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 : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : ℕ → X → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n) x = coeff n x • D.e n
i j : ℕ
⊢ (fun x ↦ x • D.e i)
      (({ toFun := coeff i, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous (‖succSub D.P i‖ / ‖D.e i‖) ⋯) (D.e j)) =
    (fun x ↦ x • D.e i) (Pi.single j 1 i)

Tactic:
by

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

Goal state before:
pp: T : ℝ
inst✝ : Fact (0 < T)
n : ℤ
⊢ ‖fourier n‖ = 1

Tactic:
by

Goal state after: