Metamath Proof Explorer


Theorem fourierdlem105

Description: A piecewise continuous function is integrable on any closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem105.p 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem105.t 𝑇 = ( 𝐵𝐴 )
fourierdlem105.m ( 𝜑𝑀 ∈ ℕ )
fourierdlem105.q ( 𝜑𝑄 ∈ ( 𝑃𝑀 ) )
fourierdlem105.f ( 𝜑𝐹 : ℝ ⟶ ℂ )
fourierdlem105.6 ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹𝑥 ) )
fourierdlem105.fcn ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
fourierdlem105.r ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim ( 𝑄𝑖 ) ) )
fourierdlem105.l ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
fourierdlem105.c ( 𝜑𝐶 ∈ ℝ )
fourierdlem105.d ( 𝜑𝐷 ∈ ( 𝐶 (,) +∞ ) )
Assertion fourierdlem105 ( 𝜑 → ( 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ↦ ( 𝐹𝑥 ) ) ∈ 𝐿1 )

Proof

Step Hyp Ref Expression
1 fourierdlem105.p 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
2 fourierdlem105.t 𝑇 = ( 𝐵𝐴 )
3 fourierdlem105.m ( 𝜑𝑀 ∈ ℕ )
4 fourierdlem105.q ( 𝜑𝑄 ∈ ( 𝑃𝑀 ) )
5 fourierdlem105.f ( 𝜑𝐹 : ℝ ⟶ ℂ )
6 fourierdlem105.6 ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹𝑥 ) )
7 fourierdlem105.fcn ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
8 fourierdlem105.r ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim ( 𝑄𝑖 ) ) )
9 fourierdlem105.l ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
10 fourierdlem105.c ( 𝜑𝐶 ∈ ℝ )
11 fourierdlem105.d ( 𝜑𝐷 ∈ ( 𝐶 (,) +∞ ) )
12 eqid ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝𝑚 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } ) = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝𝑚 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
13 eqid ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑤 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) = ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑤 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 )
14 oveq1 ( 𝑤 = 𝑦 → ( 𝑤 + ( 𝑗 · 𝑇 ) ) = ( 𝑦 + ( 𝑗 · 𝑇 ) ) )
15 14 eleq1d ( 𝑤 = 𝑦 → ( ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 ↔ ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 ) )
16 15 rexbidv ( 𝑤 = 𝑦 → ( ∃ 𝑗 ∈ ℤ ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑗 ∈ ℤ ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 ) )
17 oveq1 ( 𝑗 = 𝑘 → ( 𝑗 · 𝑇 ) = ( 𝑘 · 𝑇 ) )
18 17 oveq2d ( 𝑗 = 𝑘 → ( 𝑦 + ( 𝑗 · 𝑇 ) ) = ( 𝑦 + ( 𝑘 · 𝑇 ) ) )
19 18 eleq1d ( 𝑗 = 𝑘 → ( ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 ↔ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) )
20 19 cbvrexvw ( ∃ 𝑗 ∈ ℤ ( 𝑦 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 )
21 16 20 bitrdi ( 𝑤 = 𝑦 → ( ∃ 𝑗 ∈ ℤ ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) )
22 21 cbvrabv { 𝑤 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } = { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 }
23 22 uneq2i ( { 𝐶 , 𝐷 } ∪ { 𝑤 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
24 isoeq1 ( 𝑔 = 𝑓 → ( 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑤 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑤 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ↔ 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑤 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑤 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) )
25 24 cbviotavw ( ℩ 𝑔 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑤 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑤 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑤 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑤 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑗 ∈ ℤ ( 𝑤 + ( 𝑗 · 𝑇 ) ) ∈ ran 𝑄 } ) ) )
26 id ( 𝑤 = 𝑥𝑤 = 𝑥 )
27 oveq2 ( 𝑤 = 𝑥 → ( 𝐵𝑤 ) = ( 𝐵𝑥 ) )
28 27 oveq1d ( 𝑤 = 𝑥 → ( ( 𝐵𝑤 ) / 𝑇 ) = ( ( 𝐵𝑥 ) / 𝑇 ) )
29 28 fveq2d ( 𝑤 = 𝑥 → ( ⌊ ‘ ( ( 𝐵𝑤 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) )
30 29 oveq1d ( 𝑤 = 𝑥 → ( ( ⌊ ‘ ( ( 𝐵𝑤 ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) )
31 26 30 oveq12d ( 𝑤 = 𝑥 → ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵𝑤 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
32 31 cbvmptv ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
33 eqeq1 ( 𝑤 = 𝑦 → ( 𝑤 = 𝐵𝑦 = 𝐵 ) )
34 id ( 𝑤 = 𝑦𝑤 = 𝑦 )
35 33 34 ifbieq2d ( 𝑤 = 𝑦 → if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) = if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) )
36 35 cbvmptv ( 𝑤 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) ) = ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) )
37 fveq2 ( 𝑧 = 𝑥 → ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑧 ) = ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) )
38 37 fveq2d ( 𝑧 = 𝑥 → ( ( 𝑤 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) ) ‘ ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑧 ) ) = ( ( 𝑤 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) ) ‘ ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) )
39 38 breq2d ( 𝑧 = 𝑥 → ( ( 𝑄𝑗 ) ≤ ( ( 𝑤 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) ) ‘ ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑧 ) ) ↔ ( 𝑄𝑗 ) ≤ ( ( 𝑤 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) ) ‘ ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) ) )
40 39 rabbidv ( 𝑧 = 𝑥 → { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑗 ) ≤ ( ( 𝑤 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) ) ‘ ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑧 ) ) } = { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑗 ) ≤ ( ( 𝑤 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) ) ‘ ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) } )
41 fveq2 ( 𝑗 = 𝑖 → ( 𝑄𝑗 ) = ( 𝑄𝑖 ) )
42 41 breq1d ( 𝑗 = 𝑖 → ( ( 𝑄𝑗 ) ≤ ( ( 𝑤 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) ) ‘ ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) ↔ ( 𝑄𝑖 ) ≤ ( ( 𝑤 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) ) ‘ ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) ) )
43 42 cbvrabv { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑗 ) ≤ ( ( 𝑤 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) ) ‘ ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) } = { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑖 ) ≤ ( ( 𝑤 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) ) ‘ ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) }
44 40 43 eqtrdi ( 𝑧 = 𝑥 → { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑗 ) ≤ ( ( 𝑤 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) ) ‘ ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑧 ) ) } = { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑖 ) ≤ ( ( 𝑤 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) ) ‘ ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) } )
45 44 supeq1d ( 𝑧 = 𝑥 → sup ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑗 ) ≤ ( ( 𝑤 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) ) ‘ ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑧 ) ) } , ℝ , < ) = sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑖 ) ≤ ( ( 𝑤 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) ) ‘ ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) } , ℝ , < ) )
46 45 cbvmptv ( 𝑧 ∈ ℝ ↦ sup ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑗 ) ≤ ( ( 𝑤 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) ) ‘ ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑧 ) ) } , ℝ , < ) ) = ( 𝑥 ∈ ℝ ↦ sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑖 ) ≤ ( ( 𝑤 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑤 = 𝐵 , 𝐴 , 𝑤 ) ) ‘ ( ( 𝑤 ∈ ℝ ↦ ( 𝑤 + ( ( ⌊ ‘ ( ( 𝐵𝑤 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) } , ℝ , < ) )
47 1 2 3 4 5 6 7 8 9 10 11 12 13 23 25 32 36 46 fourierdlem100 ( 𝜑 → ( 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ↦ ( 𝐹𝑥 ) ) ∈ 𝐿1 )