Metamath Proof Explorer

Theorem fourierdlem115

Description: Fourier serier convergence, for piecewise smooth functions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem115.f ⊢ φ → F : ℝ ⟶ ℝ
fourierdlem115.t ⊢ T = 2 ⁢ π
fourierdlem115.per ⊢ φ ∧ x ∈ ℝ → F ⁡ x + T = F ⁡ x
fourierdlem115.g ⊢ G = F ℝ ′ ↾ − π π
fourierdlem115.dmdv ⊢ φ → − π π ∖ dom ⁡ G ∈ Fin
fourierdlem115.dvcn ⊢ φ → G : dom ⁡ G ⟶cn ℂ
fourierdlem115.rlim ⊢ φ ∧ x ∈ − π π ∖ dom ⁡ G → G ↾ x +∞ lim ℂ x ≠ ∅
fourierdlem115.llim ⊢ φ ∧ x ∈ − π π ∖ dom ⁡ G → G ↾ −∞ x lim ℂ x ≠ ∅
fourierdlem115.x ⊢ φ → X ∈ ℝ
fourierdlem115.l ⊢ φ → L ∈ F ↾ −∞ X lim ℂ X
fourierdlem115.r ⊢ φ → R ∈ F ↾ X +∞ lim ℂ X
fourierdlem115.a ⊢ A = n ∈ ℕ 0 ⟼ ∫ − π π F ⁡ x ⁢ cos ⁡ n ⁢ x dx π
fourierdlem115.b ⊢ B = n ∈ ℕ ⟼ ∫ − π π F ⁡ x ⁢ sin ⁡ n ⁢ x dx π
fourierdlem115.s ⊢ S = k ∈ ℕ ⟼ A ⁡ k ⁢ cos ⁡ k ⁢ X + B ⁡ k ⁢ sin ⁡ k ⁢ X
Assertion fourierdlem115 ⊢ φ → seq 1 + S ⇝ L + R 2 − A ⁡ 0 2 ∧ A ⁡ 0 2 + ∑ n ∈ ℕ A ⁡ n ⁢ cos ⁡ n ⁢ X + B ⁡ n ⁢ sin ⁡ n ⁢ X = L + R 2

Proof

Step Hyp Ref Expression
1 fourierdlem115.f ⊢ φ → F : ℝ ⟶ ℝ
2 fourierdlem115.t ⊢ T = 2 ⁢ π
3 fourierdlem115.per ⊢ φ ∧ x ∈ ℝ → F ⁡ x + T = F ⁡ x
4 fourierdlem115.g ⊢ G = F ℝ ′ ↾ − π π
5 fourierdlem115.dmdv ⊢ φ → − π π ∖ dom ⁡ G ∈ Fin
6 fourierdlem115.dvcn ⊢ φ → G : dom ⁡ G ⟶cn ℂ
7 fourierdlem115.rlim ⊢ φ ∧ x ∈ − π π ∖ dom ⁡ G → G ↾ x +∞ lim ℂ x ≠ ∅
8 fourierdlem115.llim ⊢ φ ∧ x ∈ − π π ∖ dom ⁡ G → G ↾ −∞ x lim ℂ x ≠ ∅
9 fourierdlem115.x ⊢ φ → X ∈ ℝ
10 fourierdlem115.l ⊢ φ → L ∈ F ↾ −∞ X lim ℂ X
11 fourierdlem115.r ⊢ φ → R ∈ F ↾ X +∞ lim ℂ X
12 fourierdlem115.a ⊢ A = n ∈ ℕ 0 ⟼ ∫ − π π F ⁡ x ⁢ cos ⁡ n ⁢ x dx π
13 fourierdlem115.b ⊢ B = n ∈ ℕ ⟼ ∫ − π π F ⁡ x ⁢ sin ⁡ n ⁢ x dx π
14 fourierdlem115.s ⊢ S = k ∈ ℕ ⟼ A ⁡ k ⁢ cos ⁡ k ⁢ X + B ⁡ k ⁢ sin ⁡ k ⁢ X
15 oveq1 ⊢ n = k → n ⁢ x = k ⁢ x
16 15 fveq2d ⊢ n = k → cos ⁡ n ⁢ x = cos ⁡ k ⁢ x
17 16 oveq2d ⊢ n = k → F ⁡ x ⁢ cos ⁡ n ⁢ x = F ⁡ x ⁢ cos ⁡ k ⁢ x
18 17 adantr ⊢ n = k ∧ x ∈ − π π → F ⁡ x ⁢ cos ⁡ n ⁢ x = F ⁡ x ⁢ cos ⁡ k ⁢ x
19 18 itgeq2dv ⊢ n = k → ∫ − π π F ⁡ x ⁢ cos ⁡ n ⁢ x dx = ∫ − π π F ⁡ x ⁢ cos ⁡ k ⁢ x dx
20 19 oveq1d ⊢ n = k → ∫ − π π F ⁡ x ⁢ cos ⁡ n ⁢ x dx π = ∫ − π π F ⁡ x ⁢ cos ⁡ k ⁢ x dx π
21 20 cbvmptv ⊢ n ∈ ℕ 0 ⟼ ∫ − π π F ⁡ x ⁢ cos ⁡ n ⁢ x dx π = k ∈ ℕ 0 ⟼ ∫ − π π F ⁡ x ⁢ cos ⁡ k ⁢ x dx π
22 12 21 eqtri ⊢ A = k ∈ ℕ 0 ⟼ ∫ − π π F ⁡ x ⁢ cos ⁡ k ⁢ x dx π
23 15 fveq2d ⊢ n = k → sin ⁡ n ⁢ x = sin ⁡ k ⁢ x
24 23 oveq2d ⊢ n = k → F ⁡ x ⁢ sin ⁡ n ⁢ x = F ⁡ x ⁢ sin ⁡ k ⁢ x
25 24 adantr ⊢ n = k ∧ x ∈ − π π → F ⁡ x ⁢ sin ⁡ n ⁢ x = F ⁡ x ⁢ sin ⁡ k ⁢ x
26 25 itgeq2dv ⊢ n = k → ∫ − π π F ⁡ x ⁢ sin ⁡ n ⁢ x dx = ∫ − π π F ⁡ x ⁢ sin ⁡ k ⁢ x dx
27 26 oveq1d ⊢ n = k → ∫ − π π F ⁡ x ⁢ sin ⁡ n ⁢ x dx π = ∫ − π π F ⁡ x ⁢ sin ⁡ k ⁢ x dx π
28 27 cbvmptv ⊢ n ∈ ℕ ⟼ ∫ − π π F ⁡ x ⁢ sin ⁡ n ⁢ x dx π = k ∈ ℕ ⟼ ∫ − π π F ⁡ x ⁢ sin ⁡ k ⁢ x dx π
29 13 28 eqtri ⊢ B = k ∈ ℕ ⟼ ∫ − π π F ⁡ x ⁢ sin ⁡ k ⁢ x dx π
30 eqid ⊢ k ∈ ℕ ⟼ w ∈ ℝ 0 … k | w ⁡ 0 = − π ∧ w ⁡ k = π ∧ ∀ z ∈ 0 ..^ k w ⁡ z < w ⁡ z + 1 = k ∈ ℕ ⟼ w ∈ ℝ 0 … k | w ⁡ 0 = − π ∧ w ⁡ k = π ∧ ∀ z ∈ 0 ..^ k w ⁡ z < w ⁡ z + 1
31 id ⊢ y = x → y = x
32 oveq2 ⊢ y = x → π − y = π − x
33 32 oveq1d ⊢ y = x → π − y T = π − x T
34 33 fveq2d ⊢ y = x → π − y T = π − x T
35 34 oveq1d ⊢ y = x → π − y T ⁢ T = π − x T ⁢ T
36 31 35 oveq12d ⊢ y = x → y + π − y T ⁢ T = x + π − x T ⁢ T
37 36 cbvmptv ⊢ y ∈ ℝ ⟼ y + π − y T ⁢ T = x ∈ ℝ ⟼ x + π − x T ⁢ T
38 eqid ⊢ − π π y ∈ ℝ ⟼ y + π − y T ⁢ T ⁡ X ∪ − π π ∖ dom ⁡ G = − π π y ∈ ℝ ⟼ y + π − y T ⁢ T ⁡ X ∪ − π π ∖ dom ⁡ G
39 eqid ⊢ − π π y ∈ ℝ ⟼ y + π − y T ⁢ T ⁡ X ∪ − π π ∖ dom ⁡ G − 1 = − π π y ∈ ℝ ⟼ y + π − y T ⁢ T ⁡ X ∪ − π π ∖ dom ⁡ G − 1
40 isoeq1 ⊢ g = f → g Isom < , < 0 … − π π y ∈ ℝ ⟼ y + π − y T ⁢ T ⁡ X ∪ − π π ∖ dom ⁡ G − 1 − π π y ∈ ℝ ⟼ y + π − y T ⁢ T ⁡ X ∪ − π π ∖ dom ⁡ G ↔ f Isom < , < 0 … − π π y ∈ ℝ ⟼ y + π − y T ⁢ T ⁡ X ∪ − π π ∖ dom ⁡ G − 1 − π π y ∈ ℝ ⟼ y + π − y T ⁢ T ⁡ X ∪ − π π ∖ dom ⁡ G
41 40 cbviotavw ⊢ ι g | g Isom < , < 0 … − π π y ∈ ℝ ⟼ y + π − y T ⁢ T ⁡ X ∪ − π π ∖ dom ⁡ G − 1 − π π y ∈ ℝ ⟼ y + π − y T ⁢ T ⁡ X ∪ − π π ∖ dom ⁡ G = ι f | f Isom < , < 0 … − π π y ∈ ℝ ⟼ y + π − y T ⁢ T ⁡ X ∪ − π π ∖ dom ⁡ G − 1 − π π y ∈ ℝ ⟼ y + π − y T ⁢ T ⁡ X ∪ − π π ∖ dom ⁡ G
42 1 2 3 4 5 6 7 8 9 10 11 22 29 14 30 37 38 39 41 fourierdlem114 ⊢ φ → seq 1 + S ⇝ L + R 2 − A ⁡ 0 2 ∧ A ⁡ 0 2 + ∑ k ∈ ℕ A ⁡ k ⁢ cos ⁡ k ⁢ X + B ⁡ k ⁢ sin ⁡ k ⁢ X = L + R 2
43 42 simpld ⊢ φ → seq 1 + S ⇝ L + R 2 − A ⁡ 0 2
44 nfcv ⊢ Ⅎ _ k A ⁡ n ⁢ cos ⁡ n ⁢ X + B ⁡ n ⁢ sin ⁡ n ⁢ X
45 nfmpt1 ⊢ Ⅎ _ n n ∈ ℕ 0 ⟼ ∫ − π π F ⁡ x ⁢ cos ⁡ n ⁢ x dx π
46 12 45 nfcxfr ⊢ Ⅎ _ n A
47 nfcv ⊢ Ⅎ _ n k
48 46 47 nffv ⊢ Ⅎ _ n A ⁡ k
49 nfcv ⊢ Ⅎ _ n ×
50 nfcv ⊢ Ⅎ _ n cos ⁡ k ⁢ X
51 48 49 50 nfov ⊢ Ⅎ _ n A ⁡ k ⁢ cos ⁡ k ⁢ X
52 nfcv ⊢ Ⅎ _ n +
53 nfmpt1 ⊢ Ⅎ _ n n ∈ ℕ ⟼ ∫ − π π F ⁡ x ⁢ sin ⁡ n ⁢ x dx π
54 13 53 nfcxfr ⊢ Ⅎ _ n B
55 54 47 nffv ⊢ Ⅎ _ n B ⁡ k
56 nfcv ⊢ Ⅎ _ n sin ⁡ k ⁢ X
57 55 49 56 nfov ⊢ Ⅎ _ n B ⁡ k ⁢ sin ⁡ k ⁢ X
58 51 52 57 nfov ⊢ Ⅎ _ n A ⁡ k ⁢ cos ⁡ k ⁢ X + B ⁡ k ⁢ sin ⁡ k ⁢ X
59 fveq2 ⊢ n = k → A ⁡ n = A ⁡ k
60 oveq1 ⊢ n = k → n ⁢ X = k ⁢ X
61 60 fveq2d ⊢ n = k → cos ⁡ n ⁢ X = cos ⁡ k ⁢ X
62 59 61 oveq12d ⊢ n = k → A ⁡ n ⁢ cos ⁡ n ⁢ X = A ⁡ k ⁢ cos ⁡ k ⁢ X
63 fveq2 ⊢ n = k → B ⁡ n = B ⁡ k
64 60 fveq2d ⊢ n = k → sin ⁡ n ⁢ X = sin ⁡ k ⁢ X
65 63 64 oveq12d ⊢ n = k → B ⁡ n ⁢ sin ⁡ n ⁢ X = B ⁡ k ⁢ sin ⁡ k ⁢ X
66 62 65 oveq12d ⊢ n = k → A ⁡ n ⁢ cos ⁡ n ⁢ X + B ⁡ n ⁢ sin ⁡ n ⁢ X = A ⁡ k ⁢ cos ⁡ k ⁢ X + B ⁡ k ⁢ sin ⁡ k ⁢ X
67 44 58 66 cbvsumi ⊢ ∑ n ∈ ℕ A ⁡ n ⁢ cos ⁡ n ⁢ X + B ⁡ n ⁢ sin ⁡ n ⁢ X = ∑ k ∈ ℕ A ⁡ k ⁢ cos ⁡ k ⁢ X + B ⁡ k ⁢ sin ⁡ k ⁢ X
68 67 oveq2i ⊢ A ⁡ 0 2 + ∑ n ∈ ℕ A ⁡ n ⁢ cos ⁡ n ⁢ X + B ⁡ n ⁢ sin ⁡ n ⁢ X = A ⁡ 0 2 + ∑ k ∈ ℕ A ⁡ k ⁢ cos ⁡ k ⁢ X + B ⁡ k ⁢ sin ⁡ k ⁢ X
69 42 simprd ⊢ φ → A ⁡ 0 2 + ∑ k ∈ ℕ A ⁡ k ⁢ cos ⁡ k ⁢ X + B ⁡ k ⁢ sin ⁡ k ⁢ X = L + R 2
70 68 69 eqtrid ⊢ φ → A ⁡ 0 2 + ∑ n ∈ ℕ A ⁡ n ⁢ cos ⁡ n ⁢ X + B ⁡ n ⁢ sin ⁡ n ⁢ X = L + R 2
71 43 70 jca ⊢ φ → seq 1 + S ⇝ L + R 2 − A ⁡ 0 2 ∧ A ⁡ 0 2 + ∑ n ∈ ℕ A ⁡ n ⁢ cos ⁡ n ⁢ X + B ⁡ n ⁢ sin ⁡ n ⁢ X = L + R 2