Metamath Proof Explorer

Theorem fourier2

Description: Fourier series convergence, for a piecewise smooth function. Here it is also proven the existence of the left and right limits of F at any given point X . See fourierd for a comparison. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourier2.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
fourier2.t ⊢ 𝑇 = ( 2 · π )
fourier2.per ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
fourier2.g ⊢ 𝐺 = ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) )
fourier2.dmdv ⊢ ( 𝜑 → ( ( - π (,) π ) ∖ dom 𝐺 ) ∈ Fin )
fourier2.dvcn ⊢ ( 𝜑 → 𝐺 ∈ ( dom 𝐺 –cn→ ℂ ) )
fourier2.rlim ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( - π [,) π ) ∖ dom 𝐺 ) ) → ( ( 𝐺 ↾ ( 𝑥 (,) +∞ ) ) limℂ 𝑥 ) ≠ ∅ )
fourier2.llim ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( - π (,] π ) ∖ dom 𝐺 ) ) → ( ( 𝐺 ↾ ( -∞ (,) 𝑥 ) ) limℂ 𝑥 ) ≠ ∅ )
fourier2.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
fourier2.a ⊢ 𝐴 = ( 𝑛 ∈ ℕ0 ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
fourier2.b ⊢ 𝐵 = ( 𝑛 ∈ ℕ ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
Assertion fourier2 ( 𝜑 → ∃ 𝑙 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ∃ 𝑟 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑛 ∈ ℕ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) ) = ( ( 𝑙 + 𝑟 ) / 2 ) )

Proof

Step Hyp Ref Expression
1 fourier2.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2 fourier2.t ⊢ 𝑇 = ( 2 · π )
3 fourier2.per ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
4 fourier2.g ⊢ 𝐺 = ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) )
5 fourier2.dmdv ⊢ ( 𝜑 → ( ( - π (,) π ) ∖ dom 𝐺 ) ∈ Fin )
6 fourier2.dvcn ⊢ ( 𝜑 → 𝐺 ∈ ( dom 𝐺 –cn→ ℂ ) )
7 fourier2.rlim ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( - π [,) π ) ∖ dom 𝐺 ) ) → ( ( 𝐺 ↾ ( 𝑥 (,) +∞ ) ) limℂ 𝑥 ) ≠ ∅ )
8 fourier2.llim ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( - π (,] π ) ∖ dom 𝐺 ) ) → ( ( 𝐺 ↾ ( -∞ (,) 𝑥 ) ) limℂ 𝑥 ) ≠ ∅ )
9 fourier2.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
10 fourier2.a ⊢ 𝐴 = ( 𝑛 ∈ ℕ0 ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
11 fourier2.b ⊢ 𝐵 = ( 𝑛 ∈ ℕ ↦ ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
12 1 2 3 4 5 6 7 8 9 fourierdlem106 ⊢ ( 𝜑 → ( ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ≠ ∅ ∧ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ≠ ∅ ) )
13 12 simpld ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ≠ ∅ )
14 n0 ⊢ ( ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ≠ ∅ ↔ ∃ 𝑙 𝑙 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) )
15 13 14 sylib ⊢ ( 𝜑 → ∃ 𝑙 𝑙 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) )
16 simpr ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ) → 𝑙 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) )
17 12 simprd ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ≠ ∅ )
18 n0 ⊢ ( ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ≠ ∅ ↔ ∃ 𝑟 𝑟 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) )
19 17 18 sylib ⊢ ( 𝜑 → ∃ 𝑟 𝑟 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ) → ∃ 𝑟 𝑟 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) )
21 simpr ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ) ∧ 𝑟 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ) → 𝑟 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) )
22 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ) ∧ 𝑟 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ) → 𝐹 : ℝ ⟶ ℝ )
23 3 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ) ∧ 𝑟 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
24 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ) ∧ 𝑟 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ) → ( ( - π (,) π ) ∖ dom 𝐺 ) ∈ Fin )
25 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ) ∧ 𝑟 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ) → 𝐺 ∈ ( dom 𝐺 –cn→ ℂ ) )
26 7 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ) ∧ 𝑟 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ) ∧ 𝑥 ∈ ( ( - π [,) π ) ∖ dom 𝐺 ) ) → ( ( 𝐺 ↾ ( 𝑥 (,) +∞ ) ) limℂ 𝑥 ) ≠ ∅ )
27 8 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ) ∧ 𝑟 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ) ∧ 𝑥 ∈ ( ( - π (,] π ) ∖ dom 𝐺 ) ) → ( ( 𝐺 ↾ ( -∞ (,) 𝑥 ) ) limℂ 𝑥 ) ≠ ∅ )
28 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ) ∧ 𝑟 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ) → 𝑋 ∈ ℝ )
29 16 adantr ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ) ∧ 𝑟 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ) → 𝑙 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) )
30 22 2 23 4 24 25 26 27 28 29 21 10 11 fourierd ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ) ∧ 𝑟 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ) → ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑛 ∈ ℕ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) ) = ( ( 𝑙 + 𝑟 ) / 2 ) )
31 21 30 jca ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ) ∧ 𝑟 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ) → ( 𝑟 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ∧ ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑛 ∈ ℕ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) ) = ( ( 𝑙 + 𝑟 ) / 2 ) ) )
32 31 ex ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ) → ( 𝑟 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) → ( 𝑟 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ∧ ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑛 ∈ ℕ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) ) = ( ( 𝑙 + 𝑟 ) / 2 ) ) ) )
33 32 eximdv ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ) → ( ∃ 𝑟 𝑟 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) → ∃ 𝑟 ( 𝑟 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ∧ ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑛 ∈ ℕ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) ) = ( ( 𝑙 + 𝑟 ) / 2 ) ) ) )
34 20 33 mpd ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ) → ∃ 𝑟 ( 𝑟 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ∧ ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑛 ∈ ℕ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) ) = ( ( 𝑙 + 𝑟 ) / 2 ) ) )
35 df-rex ⊢ ( ∃ 𝑟 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑛 ∈ ℕ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) ) = ( ( 𝑙 + 𝑟 ) / 2 ) ↔ ∃ 𝑟 ( 𝑟 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ∧ ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑛 ∈ ℕ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) ) = ( ( 𝑙 + 𝑟 ) / 2 ) ) )
36 34 35 sylibr ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ) → ∃ 𝑟 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑛 ∈ ℕ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) ) = ( ( 𝑙 + 𝑟 ) / 2 ) )
37 16 36 jca ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ) → ( 𝑙 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ∧ ∃ 𝑟 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑛 ∈ ℕ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) ) = ( ( 𝑙 + 𝑟 ) / 2 ) ) )
38 37 ex ⊢ ( 𝜑 → ( 𝑙 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) → ( 𝑙 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ∧ ∃ 𝑟 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑛 ∈ ℕ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) ) = ( ( 𝑙 + 𝑟 ) / 2 ) ) ) )
39 38 eximdv ⊢ ( 𝜑 → ( ∃ 𝑙 𝑙 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) → ∃ 𝑙 ( 𝑙 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ∧ ∃ 𝑟 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑛 ∈ ℕ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) ) = ( ( 𝑙 + 𝑟 ) / 2 ) ) ) )
40 15 39 mpd ⊢ ( 𝜑 → ∃ 𝑙 ( 𝑙 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ∧ ∃ 𝑟 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑛 ∈ ℕ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) ) = ( ( 𝑙 + 𝑟 ) / 2 ) ) )
41 df-rex ⊢ ( ∃ 𝑙 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ∃ 𝑟 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑛 ∈ ℕ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) ) = ( ( 𝑙 + 𝑟 ) / 2 ) ↔ ∃ 𝑙 ( 𝑙 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ∧ ∃ 𝑟 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑛 ∈ ℕ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) ) = ( ( 𝑙 + 𝑟 ) / 2 ) ) )
42 40 41 sylibr ⊢ ( 𝜑 → ∃ 𝑙 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ∃ 𝑟 ∈ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ( ( ( 𝐴 ‘ 0 ) / 2 ) + Σ 𝑛 ∈ ℕ ( ( ( 𝐴 ‘ 𝑛 ) · ( cos ‘ ( 𝑛 · 𝑋 ) ) ) + ( ( 𝐵 ‘ 𝑛 ) · ( sin ‘ ( 𝑛 · 𝑋 ) ) ) ) ) = ( ( 𝑙 + 𝑟 ) / 2 ) )