mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.InnerProductSpace.l2Space

Goal state before:
pp: case calc_1
ι : 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)

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

Tactic:
·

Goal state after:
case calc_1
ι : 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)
Module: Mathlib.Analysis.InnerProductSpace.l2Space

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

Tactic:
·

Goal state after:
case calc_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)
f g : ↥(lp G 2)
c : 𝕜
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Analysis.InnerProductSpace.l2Space

Goal state before:
pp: case pos
ι : 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)
j : ι
h : j = i
⊢ ⟪Pi.single i a j, ↑f j⟫ = ⟪a, ↑f i⟫

pp: case neg
ι : 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)
j : ι
h : ¬j = i
⊢ ⟪Pi.single i a j, ↑f j⟫ = 0

Tactic:
·

Goal state after:
case pos
ι : 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)
j : ι
h : j = i
⊢ ⟪Pi.single i a j, ↑f j⟫ = ⟪a, ↑f i⟫
Module: Mathlib.Analysis.Normed.Module.Bases

Goal state before:
pp: case hle
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
D : RankOneDecomposition 𝕜 X
n : ℕ
x : X
S : X →ₗ[𝕜] X := ⋯
hrank : Module.finrank 𝕜 ↥S.range = 1
this : FiniteDimensional 𝕜 ↥S.range
⊢ 𝕜 ∙ D.e n ≤ S.range

pp: case hd
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
D : RankOneDecomposition 𝕜 X
n : ℕ
x : X
S : X →ₗ[𝕜] X := ⋯
hrank : Module.finrank 𝕜 ↥S.range = 1
this : FiniteDimensional 𝕜 ↥S.range
⊢ Module.finrank 𝕜 ↥(𝕜 ∙ D.e n) = Module.finrank 𝕜 ↥S.range

Tactic:
·

Goal state after:
case hle
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
D : RankOneDecomposition 𝕜 X
n : ℕ
x : X
S : X →ₗ[𝕜] X := ⋯
hrank : Module.finrank 𝕜 ↥S.range = 1
this : FiniteDimensional 𝕜 ↥S.range
⊢ 𝕜 ∙ D.e n ≤ S.range
Module: Mathlib.Analysis.Normed.Module.Bases

Goal state before:
pp: case hd
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
D : RankOneDecomposition 𝕜 X
n : ℕ
x : X
S : X →ₗ[𝕜] X := ⋯
hrank : Module.finrank 𝕜 ↥S.range = 1
this : FiniteDimensional 𝕜 ↥S.range
⊢ Module.finrank 𝕜 ↥(𝕜 ∙ D.e n) = Module.finrank 𝕜 ↥S.range

Tactic:
·

Goal state after:
case hd
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
D : RankOneDecomposition 𝕜 X
n : ℕ
x : X
S : X →ₗ[𝕜] X := ⋯
hrank : Module.finrank 𝕜 ↥S.range = 1
this : FiniteDimensional 𝕜 ↥S.range
⊢ Module.finrank 𝕜 ↥(𝕜 ∙ D.e n) = Module.finrank 𝕜 ↥S.range
Module: Mathlib.Analysis.InnerProductSpace.l2Space

Goal state before:
pp: case neg
ι : 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)
j : ι
h : ¬j = i
⊢ ⟪Pi.single i a j, ↑f j⟫ = 0

Tactic:
·

Goal state after:
case neg
ι : 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)
j : ι
h : ¬j = i
⊢ ⟪Pi.single i a j, ↑f j⟫ = 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)
inst✝ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
f : ↥(lp G 2)
x✝ : ι
⊢ ‖↑f x✝‖ ^ 2 = ‖↑f x✝‖ ^ ENNReal.toReal 2

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)
⊢ 0 < ENNReal.toReal 2

Tactic:
·

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

Tactic:
·

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

Goal state before:
pp: case pos
ι : 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
j : ι
h : j = i
⊢ (V j) (Pi.single i x j) = (V i) x

pp: case neg
ι : 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
j : ι
h : ¬j = i
⊢ (V j) (Pi.single i x j) = 0

Tactic:
·

Goal state after:
case pos
ι : 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
j : ι
h : j = i
⊢ (V j) (Pi.single i x j) = (V i) x
Module: Mathlib.Analysis.InnerProductSpace.l2Space

Goal state before:
pp: case neg
ι : 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
j : ι
h : ¬j = i
⊢ (V j) (Pi.single i x j) = 0

Tactic:
·

Goal state after:
case neg
ι : 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
j : ι
h : ¬j = i
⊢ (V j) (Pi.single i x j) = 0
Module: Mathlib.Analysis.InnerProductSpace.l2Space

Goal state before:
pp: case refine_1
ι : 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)
⊢ hV.linearIsometry.range ≤ (⨆ i, (V i).range).topologicalClosure

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

Goal state after:
case refine_1
ι : 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)
⊢ hV.linearIsometry.range ≤ (⨆ i, (V i).range).topologicalClosure
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:
·

Goal state after:
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
Module: Mathlib.Analysis.InnerProductSpace.l2Space

Goal state before:
pp: case refine_2.h
ι : 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 ≤ hV.linearIsometry.range

pp: case refine_2.ht
ι : 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)
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑hV.linearIsometry.range

Tactic:
·

Goal state after:
case refine_2.h
ι : 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 ≤ hV.linearIsometry.range
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: case refine_1
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ ↑(Submonoid.closure (range fourier))
⊢ fourier 0 = 1

pp: case refine_2
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ ↑(Submonoid.closure (range fourier))
⊢ ∀ (x y : C(AddCircle T, ℂ)),
    x ∈ Submonoid.closure (range fourier) →
      y ∈ Submonoid.closure (range fourier) → x ∈ range fourier → y ∈ range fourier → x * y ∈ range fourier

Tactic:
·

Goal state after:
case refine_1
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ ↑(Submonoid.closure (range fourier))
⊢ fourier 0 = 1
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: case refine_2
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ ↑(Submonoid.closure (range fourier))
⊢ ∀ (x y : C(AddCircle T, ℂ)),
    x ∈ Submonoid.closure (range fourier) →
      y ∈ Submonoid.closure (range fourier) → x ∈ range fourier → y ∈ range fourier → x * y ∈ range fourier

Tactic:
·

Goal state after:
case refine_2
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ ↑(Submonoid.closure (range fourier))
⊢ ∀ (x y : C(AddCircle T, ℂ)),
    x ∈ Submonoid.closure (range fourier) →
      y ∈ Submonoid.closure (range fourier) → x ∈ range fourier → y ∈ range fourier → x * y ∈ range fourier
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: case pos
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : i = j
⊢ ∫ (x : AddCircle T), (fourier (j + -i)) x ∂haarAddCircle = 1

pp: case neg
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : ¬i = j
⊢ ∫ (x : AddCircle T), (fourier (j + -i)) x ∂haarAddCircle = 0

Tactic:
·

Goal state after:
case pos
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : i = j
⊢ ∫ (x : AddCircle T), (fourier (j + -i)) x ∂haarAddCircle = 1
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: case hφ1
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : AddCircle T → E
hf : Integrable f haarAddCircle
n : ℤ
⊢ AEStronglyMeasurable (⇑(fourier n)) haarAddCircle

pp: case hφ2
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : AddCircle T → E
hf : Integrable f haarAddCircle
n : ℤ
⊢ ∀ᵐ (a : AddCircle T) ∂haarAddCircle, ‖(fourier n) a‖ ≤ 1

Tactic:
·

Goal state after:
case hφ1
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : AddCircle T → E
hf : Integrable f haarAddCircle
n : ℤ
⊢ AEStronglyMeasurable (⇑(fourier n)) haarAddCircle
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: case hφ2
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : AddCircle T → E
hf : Integrable f haarAddCircle
n : ℤ
⊢ ∀ᵐ (a : AddCircle T) ∂haarAddCircle, ‖(fourier n) a‖ ≤ 1

Tactic:
·

Goal state after:
case hφ2
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : AddCircle T → E
hf : Integrable f haarAddCircle
n : ℤ
⊢ ∀ᵐ (a : AddCircle T) ∂haarAddCircle, ‖(fourier n) a‖ ≤ 1
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
⊢ (1 / (b - a)) • ∫ (x : ℝ) in a..a + b - a, (fourier (-n)) ↑x • liftIoc (b - a) a f ↑x =
    (1 / (b - a)) • ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • f x

Tactic:
add_sub_cancel_left

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
⊢ (1 / (b - a)) • ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • liftIoc (b - a) a f ↑x =
    (1 / (b - a)) • ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • f x
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: case e_a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
x : ℝ
hx : x ∈ Ioc a b
⊢ x ∈ Ioc a (a + b - a)

Tactic:
add_sub_cancel_left

Goal state after:
case e_a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
x : ℝ
hx : x ∈ Ioc a b
⊢ x ∈ Ioc a b
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ (1 / T) • ∫ (x : ℝ) in ?a..?a + T, (fourier (-n)) ↑x • liftIoc T a f ↑x =
    (1 / T) • ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • f x

pp: case a
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ ℝ

Tactic:
·

Goal state after:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ (1 / T) • ∫ (x : ℝ) in ?a..?a + T, (fourier (-n)) ↑x • liftIoc T a f ↑x =
    (1 / T) • ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • f x
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
⊢ ↑(fourierBasis.repr f) i = ∫ (t : AddCircle T), (starRingEnd ℂ) (↑↑(fourierLp 2 i) t) * ↑↑f t ∂haarAddCircle

pp: T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
⊢ ∫ (t : AddCircle T), (starRingEnd ℂ) (↑↑(fourierLp 2 i) t) * ↑↑f t ∂haarAddCircle = fourierCoeff (↑↑f) i

Tactic:
·

Goal state after:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
⊢ ↑(fourierBasis.repr f) i = ∫ (t : AddCircle T), (starRingEnd ℂ) (↑↑(fourierLp 2 i) t) * ↑↑f t ∂haarAddCircle
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
⊢ ∫ (t : AddCircle T), (starRingEnd ℂ) (↑↑(fourierLp 2 i) t) * ↑↑f t ∂haarAddCircle = fourierCoeff (↑↑f) i

Tactic:
·

Goal state after:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
⊢ ∫ (t : AddCircle T), (starRingEnd ℂ) (↑↑(fourierLp 2 i) t) * ↑↑f t ∂haarAddCircle = fourierCoeff (↑↑f) i
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
H₁ : HasSum (fun i ↦ ‖↑(fourierBasis.repr f) i‖ ^ 2) (‖fourierBasis.repr f‖ ^ 2)
H₂ : ‖fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2
H₃ : RCLike.re (inner ℂ f f) = ∫ (x : AddCircle T), RCLike.re (inner ℂ (↑↑f x) (↑↑f x)) ∂haarAddCircle
⊢ HasSum (fun i ↦ ‖↑(fourierBasis.repr f) i‖ ^ 2) (∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle)

pp: T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
H₁ : HasSum (fun i ↦ ‖↑(fourierBasis.repr f) i‖ ^ 2) (‖fourierBasis.repr f‖ ^ 2)
H₂ : ‖fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2
H₃ : RCLike.re (inner ℂ f f) = RCLike.re (∫ (a : AddCircle T), inner ℂ (↑↑f a) (↑↑f a) ∂haarAddCircle)
⊢ Integrable (fun a ↦ inner ℂ (↑↑f a) (↑↑f a)) haarAddCircle

Tactic:
·

Goal state after:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
H₁ : HasSum (fun i ↦ ‖↑(fourierBasis.repr f) i‖ ^ 2) (‖fourierBasis.repr f‖ ^ 2)
H₂ : ‖fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2
H₃ : RCLike.re (inner ℂ f f) = ∫ (x : AddCircle T), RCLike.re (inner ℂ (↑↑f x) (↑↑f x)) ∂haarAddCircle
⊢ HasSum (fun i ↦ ‖↑(fourierBasis.repr f) i‖ ^ 2) (∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle)
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
H₁ : HasSum (fun i ↦ ‖↑(fourierBasis.repr f) i‖ ^ 2) (‖fourierBasis.repr f‖ ^ 2)
H₂ : ‖fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2
H₃ : RCLike.re (inner ℂ f f) = RCLike.re (∫ (a : AddCircle T), inner ℂ (↑↑f a) (↑↑f a) ∂haarAddCircle)
⊢ Integrable (fun a ↦ inner ℂ (↑↑f a) (↑↑f a)) haarAddCircle

Tactic:
·

Goal state after:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
H₁ : HasSum (fun i ↦ ‖↑(fourierBasis.repr f) i‖ ^ 2) (‖fourierBasis.repr f‖ ^ 2)
H₂ : ‖fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2
H₃ : RCLike.re (inner ℂ f f) = RCLike.re (∫ (a : AddCircle T), inner ℂ (↑↑f a) (↑↑f a) ∂haarAddCircle)
⊢ Integrable (fun a ↦ inner ℂ (↑↑f a) (↑↑f a)) haarAddCircle
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: case e'_5
a b : ℝ
f : ℝ → ℂ
hab : a < b
hL2 : MemLp f 2 (volume.restrict (Ioc a (a + (b - a))))
this : Fact (0 < b - a)
h : MemLp (liftIoc (b - a) a f) 2 haarAddCircle
x✝ : ℤ
⊢ fourierCoeffOn hab f x✝ = fourierCoeff (↑↑(MemLp.toLp (liftIoc (b - a) a f) h)) x✝

pp: case e'_6
a b : ℝ
f : ℝ → ℂ
hab : a < b
hL2 : MemLp f 2 (volume.restrict (Ioc a (a + (b - a))))
this : Fact (0 < b - a)
h : MemLp (liftIoc (b - a) a f) 2 haarAddCircle
⊢ (b - a)⁻¹ • ∫ (x : ℝ) in a..b, ‖f x‖ ^ 2 =
    ∫ (t : AddCircle (b - a)), ‖↑↑(MemLp.toLp (liftIoc (b - a) a f) h) t‖ ^ 2 ∂haarAddCircle

Tactic:
·

Goal state after:
case e'_5
a b : ℝ
f : ℝ → ℂ
hab : a < b
hL2 : MemLp f 2 (volume.restrict (Ioc a (a + (b - a))))
this : Fact (0 < b - a)
h : MemLp (liftIoc (b - a) a f) 2 haarAddCircle
x✝ : ℤ
⊢ fourierCoeffOn hab f x✝ = fourierCoeff (↑↑(MemLp.toLp (liftIoc (b - a) a f) h)) x✝
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: case e'_6
a b : ℝ
f : ℝ → ℂ
hab : a < b
hL2 : MemLp f 2 (volume.restrict (Ioc a (a + (b - a))))
this : Fact (0 < b - a)
h : MemLp (liftIoc (b - a) a f) 2 haarAddCircle
⊢ (b - a)⁻¹ • ∫ (x : ℝ) in a..b, ‖f x‖ ^ 2 =
    ∫ (t : AddCircle (b - a)), ‖↑↑(MemLp.toLp (liftIoc (b - a) a f) h) t‖ ^ 2 ∂haarAddCircle

Tactic:
·

Goal state after:
case e'_6
a b : ℝ
f : ℝ → ℂ
hab : a < b
hL2 : MemLp f 2 (volume.restrict (Ioc a (a + (b - a))))
this : Fact (0 < b - a)
h : MemLp (liftIoc (b - a) a f) 2 haarAddCircle
⊢ (b - a)⁻¹ • ∫ (x : ℝ) in a..b, ‖f x‖ ^ 2 =
    ∫ (t : AddCircle (b - a)), ‖↑↑(MemLp.toLp (liftIoc (b - a) a f) h) t‖ ^ 2 ∂haarAddCircle
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: case inl
T : ℝ
hT : Fact (0 < T)
m : ℤ
⊢ inner ℂ (fourierLp 2 m) (fourierLp 2 m) = Pi.single m 1 m

pp: case inr
T : ℝ
hT : Fact (0 < T)
n m : ℤ
hmn : m ≠ n
⊢ inner ℂ (fourierLp 2 m) (fourierLp 2 n) = Pi.single n 1 m

Tactic:
·

Goal state after:
case inl
T : ℝ
hT : Fact (0 < T)
m : ℤ
⊢ inner ℂ (fourierLp 2 m) (fourierLp 2 m) = Pi.single m 1 m
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: case inr
T : ℝ
hT : Fact (0 < T)
n m : ℤ
hmn : m ≠ n
⊢ inner ℂ (fourierLp 2 m) (fourierLp 2 n) = Pi.single n 1 m

Tactic:
·

Goal state after:
case inr
T : ℝ
hT : Fact (0 < T)
n m : ℤ
hmn : m ≠ n
⊢ inner ℂ (fourierLp 2 m) (fourierLp 2 n) = Pi.single n 1 m
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: case e'_8
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x : ℝ
⊢ (fun y ↦ ↑T / (-2 * ↑π * I * ↑n) * (fourier (-n)) ↑y) = fun x ↦ (fourier (-n)) ↑x / (-2 * ↑π * I * ↑n / ↑T)

pp: case e'_9
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x : ℝ
⊢ (fourier (-n)) ↑x = -2 * ↑π * I * ↑n / ↑T * (fourier (-n)) ↑x / (-2 * ↑π * I * ↑n / ↑T)

Tactic:
·

Goal state after:
case e'_8
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x : ℝ
⊢ (fun y ↦ ↑T / (-2 * ↑π * I * ↑n) * (fourier (-n)) ↑y) = fun x ↦ (fourier (-n)) ↑x / (-2 * ↑π * I * ↑n / ↑T)
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: case e'_9
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x : ℝ
⊢ (fourier (-n)) ↑x = -2 * ↑π * I * ↑n / ↑T * (fourier (-n)) ↑x / (-2 * ↑π * I * ↑n / ↑T)

Tactic:
·

Goal state after:
case e'_9
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x : ℝ
⊢ (fourier (-n)) ↑x = -2 * ↑π * I * ↑n / ↑T * (fourier (-n)) ↑x / (-2 * ↑π * I * ↑n / ↑T)