![]() |
Metamath
Proof Explorer Theorem List (p. 462 of 491) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fourierdlem39 46101* | Integration by parts of ∫(𝐴(,)𝐵)((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))) d𝑥 (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) & ⊢ 𝐺 = (ℝ D 𝐹) & ⊢ (𝜑 → 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ)) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺‘𝑥)) ≤ 𝑦) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∫(𝐴(,)𝐵)((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))) d𝑥 = ((((𝐹‘𝐵) · -((cos‘(𝑅 · 𝐵)) / 𝑅)) − ((𝐹‘𝐴) · -((cos‘(𝑅 · 𝐴)) / 𝑅))) − ∫(𝐴(,)𝐵)((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) d𝑥)) | ||
Theorem | fourierdlem40 46102* | 𝐻 is a continuous function on any partition interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝐴 ∈ (-π[,]π)) & ⊢ (𝜑 → 𝐵 ∈ (-π[,]π)) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → ¬ 0 ∈ (𝐴(,)𝐵)) & ⊢ (𝜑 → (𝐹 ↾ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋))) ∈ (((𝐴 + 𝑋)(,)(𝐵 + 𝑋))–cn→ℂ)) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 𝑊 ∈ ℝ) & ⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ⇒ ⊢ (𝜑 → (𝐻 ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | ||
Theorem | fourierdlem41 46103* | Lemma used to prove that every real is a limit point for the domain of the derivative of the periodic function to be approximated. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ 𝑇 = (𝐵 − 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ 𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) & ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍‘𝑥))) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷) ⇒ ⊢ (𝜑 → (∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷) ∧ ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷))) | ||
Theorem | fourierdlem42 46104* | The set of points in a moved partition are finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 29-Sep-2020.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 < 𝐶) & ⊢ 𝑇 = (𝐶 − 𝐵) & ⊢ (𝜑 → 𝐴 ⊆ (𝐵[,]𝐶)) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ 𝐷 = (abs ∘ − ) & ⊢ 𝐼 = ((𝐴 × 𝐴) ∖ I ) & ⊢ 𝑅 = ran (𝐷 ↾ 𝐼) & ⊢ 𝐸 = inf(𝑅, ℝ, < ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐾 = (𝐽 ↾t (𝑋[,]𝑌)) & ⊢ 𝐻 = {𝑥 ∈ (𝑋[,]𝑌) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐴} & ⊢ (𝜓 ↔ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑎 < 𝑏)) ∧ ∃𝑗 ∈ ℤ ∃𝑘 ∈ ℤ ((𝑎 + (𝑗 · 𝑇)) ∈ 𝐴 ∧ (𝑏 + (𝑘 · 𝑇)) ∈ 𝐴))) ⇒ ⊢ (𝜑 → 𝐻 ∈ Fin) | ||
Theorem | fourierdlem43 46105 | 𝐾 is a real function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ⇒ ⊢ 𝐾:(-π[,]π)⟶ℝ | ||
Theorem | fourierdlem44 46106 | A condition for having (sin‘(𝐴 / 2)) nonzero. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ (-π[,]π) ∧ 𝐴 ≠ 0) → (sin‘(𝐴 / 2)) ≠ 0) | ||
Theorem | fourierdlem46 46107* | The function 𝐹 has a limit at the bounds of every interval induced by the partition 𝑄. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹 ∈ (dom 𝐹–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐹)) → ((𝐹 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐹)) → ((𝐹 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅) & ⊢ (𝜑 → 𝑄 Isom < , < ((0...𝑀), 𝐻)) & ⊢ (𝜑 → 𝑄:(0...𝑀)⟶𝐻) & ⊢ (𝜑 → 𝐼 ∈ (0..^𝑀)) & ⊢ (𝜑 → (𝑄‘𝐼) < (𝑄‘(𝐼 + 1))) & ⊢ (𝜑 → ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ (-π(,)π)) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ 𝐻 = ({-π, π, 𝐶} ∪ ((-π[,]π) ∖ dom 𝐹)) & ⊢ (𝜑 → ran 𝑄 = 𝐻) ⇒ ⊢ (𝜑 → (((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼)) ≠ ∅ ∧ ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) ≠ ∅)) | ||
Theorem | fourierdlem47 46108* | For 𝑟 large enough, the final expression is less than the given positive 𝐸. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝐹) ∈ 𝐿1) & ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ) → (𝑥 ∈ 𝐼 ↦ (𝐹 · -𝐺)) ∈ 𝐿1) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐹 ∈ ℂ) & ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑟 ∈ ℂ) → 𝐺 ∈ ℂ) & ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑟 ∈ ℝ) → (abs‘𝐺) ≤ 1) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ 𝑋 = (abs‘𝐴) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ 𝑌 = (abs‘𝐶) & ⊢ 𝑍 = ∫𝐼(abs‘𝐹) d𝑥 & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ ((𝜑 ∧ 𝑟 ∈ ℂ) → 𝐵 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ) → (abs‘𝐵) ≤ 1) & ⊢ ((𝜑 ∧ 𝑟 ∈ ℂ) → 𝐷 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ) → (abs‘𝐷) ≤ 1) & ⊢ 𝑀 = ((⌊‘((((𝑋 + 𝑌) + 𝑍) / 𝐸) + 1)) + 1) ⇒ ⊢ (𝜑 → ∃𝑚 ∈ ℕ ∀𝑟 ∈ (𝑚(,)+∞)(abs‘(((𝐴 · -(𝐵 / 𝑟)) − (𝐶 · -(𝐷 / 𝑟))) − ∫𝐼(𝐹 · -(𝐺 / 𝑟)) d𝑥)) < 𝐸) | ||
Theorem | fourierdlem48 46109* | The given periodic function 𝐹 has a right limit at every point in the reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝑇 = (𝐵 − 𝐴) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ (𝜑 → 𝐹:𝐷⟶ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ 𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) & ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍‘𝑥))) & ⊢ (𝜒 ↔ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ ℤ) ∧ 𝑦 = (𝑋 + (𝑘 · 𝑇)))) ⇒ ⊢ (𝜑 → ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋) ≠ ∅) | ||
Theorem | fourierdlem49 46110* | The given periodic function 𝐹 has a left limit at every point in the reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝑇 = (𝐵 − 𝐴) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ (𝜑 → 𝐷 ⊆ ℝ) & ⊢ (𝜑 → 𝐹:𝐷⟶ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ 𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) & ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍‘𝑥))) ⇒ ⊢ (𝜑 → ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋) ≠ ∅) | ||
Theorem | fourierdlem50 46111* | Continuity of 𝑂 and its limits with respect to the 𝑆 partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝‘𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀)) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π)) & ⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋)) & ⊢ 𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) & ⊢ 𝑁 = ((♯‘𝑇) − 1) & ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇)) & ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁)) & ⊢ 𝑈 = (℩𝑖 ∈ (0..^𝑀)((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) & ⊢ (𝜒 ↔ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑘)(,)(𝑄‘(𝑘 + 1))))) ⇒ ⊢ (𝜑 → (𝑈 ∈ (0..^𝑀) ∧ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑈)(,)(𝑄‘(𝑈 + 1))))) | ||
Theorem | fourierdlem51 46112* | 𝑋 is in the periodic partition, when the considered interval is centered at 𝑋. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 0) & ⊢ (𝜑 → 0 < 𝐵) & ⊢ 𝑇 = (𝐵 − 𝐴) & ⊢ (𝜑 → 𝐶 ∈ Fin) & ⊢ (𝜑 → 𝐶 ⊆ (𝐴[,]𝐵)) & ⊢ (𝜑 → 𝐵 ∈ 𝐶) & ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → (𝐸‘𝑋) ∈ 𝐶) & ⊢ 𝐷 = ({(𝐴 + 𝑋), (𝐵 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}) & ⊢ 𝐹 = (℩𝑓𝑓 Isom < , < ((0...((♯‘𝐷) − 1)), 𝐷)) & ⊢ 𝐻 = {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ⇒ ⊢ (𝜑 → 𝑋 ∈ ran 𝐹) | ||
Theorem | fourierdlem52 46113* | d16:d17,d18:jca |- ( ph -> ( ( S 0) ≤ 𝐴 ∧ 𝐴 ≤ (𝑆 0 ) ) ) . (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝑇 ∈ Fin) & ⊢ 𝑁 = ((♯‘𝑇) − 1) & ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇)) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑇 ⊆ (𝐴[,]𝐵)) & ⊢ (𝜑 → 𝐴 ∈ 𝑇) & ⊢ (𝜑 → 𝐵 ∈ 𝑇) ⇒ ⊢ (𝜑 → ((𝑆:(0...𝑁)⟶(𝐴[,]𝐵) ∧ (𝑆‘0) = 𝐴) ∧ (𝑆‘𝑁) = 𝐵)) | ||
Theorem | fourierdlem53 46114* | The limit of 𝐹(𝑠) at (𝑋 + 𝐷) is the limit of 𝐹(𝑋 + 𝑠) at 𝐷. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ 𝐺 = (𝑠 ∈ 𝐴 ↦ (𝐹‘(𝑋 + 𝑠))) & ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (𝑋 + 𝑠) ∈ 𝐵) & ⊢ (𝜑 → 𝐵 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑠 ≠ 𝐷) & ⊢ (𝜑 → 𝐶 ∈ ((𝐹 ↾ 𝐵) limℂ (𝑋 + 𝐷))) & ⊢ (𝜑 → 𝐷 ∈ ℂ) ⇒ ⊢ (𝜑 → 𝐶 ∈ (𝐺 limℂ 𝐷)) | ||
Theorem | fourierdlem54 46115* | Given a partition 𝑄 and an arbitrary interval [𝐶, 𝐷], a partition 𝑆 on [𝐶, 𝐷] is built such that it preserves any periodic function piecewise continuous on 𝑄 will be piecewise continuous on 𝑆, with the same limits. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝑇 = (𝐵 − 𝐴) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐶 < 𝐷) & ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) & ⊢ 𝑁 = ((♯‘𝐻) − 1) & ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻)) ⇒ ⊢ (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻))) | ||
Theorem | fourierdlem55 46116* | 𝑈 is a real function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 𝑊 ∈ ℝ) & ⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) & ⊢ 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) & ⊢ 𝑈 = (𝑠 ∈ (-π[,]π) ↦ ((𝐻‘𝑠) · (𝐾‘𝑠))) ⇒ ⊢ (𝜑 → 𝑈:(-π[,]π)⟶ℝ) | ||
Theorem | fourierdlem56 46117* | Derivative of the 𝐾 function on an interval not containing ' 0 '. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) & ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ((-π[,]π) ∖ {0})) & ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ≠ 0) ⇒ ⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐾‘𝑠))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((((sin‘(𝑠 / 2)) − (((cos‘(𝑠 / 2)) / 2) · 𝑠)) / ((sin‘(𝑠 / 2))↑2)) / 2))) | ||
Theorem | fourierdlem57 46118* | The derivative of 𝑂. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐵))⟶ℝ) & ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (-π[,]π)) & ⊢ (𝜑 → ¬ 0 ∈ (𝐴(,)𝐵)) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ 𝑂 = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))) ⇒ ⊢ ((𝜑 → ((ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ ∧ (ℝ D 𝑂) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2))))) ∧ (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑠 / 2)))) | ||
Theorem | fourierdlem58 46119* | The derivative of 𝐾 is continuous on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐾 = (𝑠 ∈ 𝐴 ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) & ⊢ (𝜑 → 𝐴 ⊆ (-π[,]π)) & ⊢ (𝜑 → ¬ 0 ∈ 𝐴) & ⊢ (𝜑 → 𝐴 ∈ (topGen‘ran (,))) ⇒ ⊢ (𝜑 → (ℝ D 𝐾) ∈ (𝐴–cn→ℝ)) | ||
Theorem | fourierdlem59 46120* | The derivative of 𝐻 is continuous on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ¬ 0 ∈ (𝐴(,)𝐵)) & ⊢ (𝜑 → (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))) ∈ (((𝑋 + 𝐴)(,)(𝑋 + 𝐵))–cn→ℝ)) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ 𝐻 = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) ⇒ ⊢ (𝜑 → (ℝ D 𝐻) ∈ ((𝐴(,)𝐵)–cn→ℝ)) | ||
Theorem | fourierdlem60 46121* | Given a differentiable function 𝐹, with finite limit of the derivative at 𝐴 the derived function 𝐻 has a limit at 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ) & ⊢ (𝜑 → 𝑌 ∈ (𝐹 limℂ 𝐵)) & ⊢ 𝐺 = (ℝ D 𝐹) & ⊢ (𝜑 → dom 𝐺 = (𝐴(,)𝐵)) & ⊢ (𝜑 → 𝐸 ∈ (𝐺 limℂ 𝐵)) & ⊢ 𝐻 = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (((𝐹‘(𝐵 + 𝑠)) − 𝑌) / 𝑠)) & ⊢ 𝑁 = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐹‘(𝐵 + 𝑠)) − 𝑌)) & ⊢ 𝐷 = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 𝑠) ⇒ ⊢ (𝜑 → 𝐸 ∈ (𝐻 limℂ 0)) | ||
Theorem | fourierdlem61 46122* | Given a differentiable function 𝐹, with finite limit of the derivative at 𝐴 the derived function 𝐻 has a limit at 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ) & ⊢ (𝜑 → 𝑌 ∈ (𝐹 limℂ 𝐴)) & ⊢ 𝐺 = (ℝ D 𝐹) & ⊢ (𝜑 → dom 𝐺 = (𝐴(,)𝐵)) & ⊢ (𝜑 → 𝐸 ∈ (𝐺 limℂ 𝐴)) & ⊢ 𝐻 = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (((𝐹‘(𝐴 + 𝑠)) − 𝑌) / 𝑠)) & ⊢ 𝑁 = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌)) & ⊢ 𝐷 = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 𝑠) ⇒ ⊢ (𝜑 → 𝐸 ∈ (𝐻 limℂ 0)) | ||
Theorem | fourierdlem62 46123 | The function 𝐾 is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐾 = (𝑦 ∈ (-π[,]π) ↦ if(𝑦 = 0, 1, (𝑦 / (2 · (sin‘(𝑦 / 2)))))) ⇒ ⊢ 𝐾 ∈ ((-π[,]π)–cn→ℝ) | ||
Theorem | fourierdlem63 46124* | The upper bound of intervals in the moved partition are mapped to points that are not greater than the corresponding upper bounds in the original partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝑇 = (𝐵 − 𝐴) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐶 < 𝐷) & ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) & ⊢ 𝑁 = ((♯‘𝐻) − 1) & ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻)) & ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) & ⊢ (𝜑 → 𝐾 ∈ (0...𝑀)) & ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁)) & ⊢ (𝜑 → 𝑌 ∈ ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1)))) & ⊢ (𝜑 → (𝐸‘𝑌) < (𝑄‘𝐾)) & ⊢ 𝑋 = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ⇒ ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ≤ (𝑄‘𝐾)) | ||
Theorem | fourierdlem64 46125* | The partition 𝑉 is finer than 𝑄, when 𝑄 is moved on the same interval where 𝑉 lies. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝑇 = (𝐵 − 𝐴) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐶 < 𝐷) & ⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) & ⊢ 𝑁 = ((♯‘𝐻) − 1) & ⊢ 𝑉 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻)) & ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁)) & ⊢ 𝐿 = sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) & ⊢ 𝐼 = sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ⇒ ⊢ (𝜑 → ((𝐼 ∈ (0..^𝑀) ∧ 𝐿 ∈ ℤ) ∧ ∃𝑖 ∈ (0..^𝑀)∃𝑙 ∈ ℤ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))) | ||
Theorem | fourierdlem65 46126* | The distance of two adjacent points in the moved partition is preserved in the original partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝑇 = (𝐵 − 𝐴) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ (𝐶(,)+∞)) & ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝑁 = ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})) − 1) & ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}))) & ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) & ⊢ 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)) & ⊢ 𝑍 = ((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗)))) ⇒ ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝐿‘(𝐸‘(𝑆‘𝑗)))) = ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗))) | ||
Theorem | fourierdlem66 46127* | Value of the 𝐺 function when the argument is not zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 𝑊 ∈ ℝ) & ⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑠 ∈ ℝ ↦ if((𝑠 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) · (sin‘(𝑠 / 2))))))) & ⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) & ⊢ 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) & ⊢ 𝑈 = (𝑠 ∈ (-π[,]π) ↦ ((𝐻‘𝑠) · (𝐾‘𝑠))) & ⊢ 𝑆 = (𝑠 ∈ (-π[,]π) ↦ (sin‘((𝑛 + (1 / 2)) · 𝑠))) & ⊢ 𝐺 = (𝑠 ∈ (-π[,]π) ↦ ((𝑈‘𝑠) · (𝑆‘𝑠))) & ⊢ 𝐴 = ((-π[,]π) ∖ {0}) ⇒ ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → (𝐺‘𝑠) = (π · (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠)))) | ||
Theorem | fourierdlem67 46128* | 𝐺 is a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 𝑊 ∈ ℝ) & ⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) & ⊢ 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) & ⊢ 𝑈 = (𝑠 ∈ (-π[,]π) ↦ ((𝐻‘𝑠) · (𝐾‘𝑠))) & ⊢ (𝜑 → 𝑁 ∈ ℝ) & ⊢ 𝑆 = (𝑠 ∈ (-π[,]π) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑠))) & ⊢ 𝐺 = (𝑠 ∈ (-π[,]π) ↦ ((𝑈‘𝑠) · (𝑆‘𝑠))) ⇒ ⊢ (𝜑 → 𝐺:(-π[,]π)⟶ℝ) | ||
Theorem | fourierdlem68 46129* | The derivative of 𝑂 is bounded on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π)) & ⊢ (𝜑 → ¬ 0 ∈ (𝐴[,]𝐵)) & ⊢ (𝜑 → (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐵))⟶ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘(𝐹‘𝑡)) ≤ 𝐷) & ⊢ (𝜑 → 𝐸 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘𝑡)) ≤ 𝐸) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ 𝑂 = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))) ⇒ ⊢ (𝜑 → (dom (ℝ D 𝑂) = (𝐴(,)𝐵) ∧ ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑏)) | ||
Theorem | fourierdlem69 46130* | A piecewise continuous function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) ⇒ ⊢ (𝜑 → 𝐹 ∈ 𝐿1) | ||
Theorem | fourierdlem70 46131* | A piecewise continuous function is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ) & ⊢ (𝜑 → (𝑄‘0) = 𝐴) & ⊢ (𝜑 → (𝑄‘𝑀) = 𝐵) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) & ⊢ 𝐼 = (𝑖 ∈ (0..^𝑀) ↦ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑠 ∈ (𝐴[,]𝐵)(abs‘(𝐹‘𝑠)) ≤ 𝑥) | ||
Theorem | fourierdlem71 46132* | A periodic piecewise continuous function, possibly undefined on a finite set in each periodic interval, is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → dom 𝐹 ⊆ ℝ) & ⊢ (𝜑 → 𝐹:dom 𝐹⟶ℝ) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ 𝑇 = (𝐵 − 𝐴) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ) & ⊢ (𝜑 → (𝑄‘0) = 𝐴) & ⊢ (𝜑 → (𝑄‘𝑀) = 𝐵) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) & ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ dom 𝐹) & ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘𝑥)) & ⊢ 𝐼 = (𝑖 ∈ (0..^𝑀) ↦ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) & ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ dom 𝐹(abs‘(𝐹‘𝑥)) ≤ 𝑦) | ||
Theorem | fourierdlem72 46133* | The derivative of 𝑂 is continuous on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝‘𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℝ)) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (-π[,]π)) & ⊢ (𝜑 → ¬ 0 ∈ (𝐴[,]𝐵)) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋)) & ⊢ (𝜑 → 𝑈 ∈ (0..^𝑀)) & ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ((𝑄‘𝑈)(,)(𝑄‘(𝑈 + 1)))) & ⊢ 𝐻 = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) & ⊢ 𝐾 = (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) & ⊢ 𝑂 = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐻‘𝑠) · (𝐾‘𝑠))) ⇒ ⊢ (𝜑 → (ℝ D 𝑂) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | ||
Theorem | fourierdlem73 46134* | A version of the Riemann Lebesgue lemma: as 𝑟 increases, the integral in 𝑆 goes to zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵)) & ⊢ (𝜑 → (𝑄‘0) = 𝐴) & ⊢ (𝜑 → (𝑄‘𝑀) = 𝐵) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) & ⊢ 𝐺 = (ℝ D 𝐹) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ dom 𝐺(abs‘(𝐺‘𝑥)) ≤ 𝑦) & ⊢ 𝑆 = (𝑟 ∈ ℝ+ ↦ ∫(𝐴(,)𝐵)((𝐹‘𝑥) · (sin‘(𝑟 · 𝑥))) d𝑥) & ⊢ 𝐷 = (𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘𝑥)))) ⇒ ⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)(abs‘∫(𝐴(,)𝐵)((𝐹‘𝑥) · (sin‘(𝑟 · 𝑥))) d𝑥) < 𝑒) | ||
Theorem | fourierdlem74 46135* | Given a piecewise smooth function 𝐹, the derived function 𝐻 has a limit at the upper bound of each interval of the partition 𝑄. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝‘𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝑋 ∈ ran 𝑉) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 𝑊 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) & ⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) limℂ (𝑉‘(𝑖 + 1)))) & ⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋)) & ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝐺 = (ℝ D 𝐹) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℝ) & ⊢ (𝜑 → 𝐸 ∈ ((𝐺 ↾ (-∞(,)𝑋)) limℂ 𝑋)) & ⊢ 𝐴 = if((𝑉‘(𝑖 + 1)) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1)))) ⇒ ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) | ||
Theorem | fourierdlem75 46136* | Given a piecewise smooth function 𝐹, the derived function 𝐻 has a limit at the lower bound of each interval of the partition 𝑄. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝‘𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝑋 ∈ ran 𝑉) & ⊢ (𝜑 → 𝑌 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) & ⊢ (𝜑 → 𝑊 ∈ ℝ) & ⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) limℂ (𝑉‘𝑖))) & ⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋)) & ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝐺 = (ℝ D 𝐹) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℂ) & ⊢ (𝜑 → 𝐸 ∈ ((𝐺 ↾ (𝑋(,)+∞)) limℂ 𝑋)) & ⊢ 𝐴 = if((𝑉‘𝑖) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) / (𝑄‘𝑖))) ⇒ ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) | ||
Theorem | fourierdlem76 46137* | Continuity of 𝑂 and its limits with respect to the 𝑆 partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝‘𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) limℂ (𝑉‘𝑖))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) limℂ (𝑉‘(𝑖 + 1)))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π)) & ⊢ (𝜑 → ¬ 0 ∈ (𝐴[,]𝐵)) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ 𝑂 = (𝑠 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) & ⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋)) & ⊢ 𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) & ⊢ 𝑁 = ((♯‘𝑇) − 1) & ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇)) & ⊢ 𝐷 = (((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) · ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))))) & ⊢ 𝐸 = (((if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) · ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2))))) & ⊢ (𝜒 ↔ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) ⇒ ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐷 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) limℂ (𝑆‘(𝑗 + 1))) ∧ 𝐸 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) limℂ (𝑆‘𝑗))) ∧ (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))) | ||
Theorem | fourierdlem77 46138* | If 𝐻 is bounded, then 𝑈 is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 𝑊 ∈ ℝ) & ⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) & ⊢ 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) & ⊢ 𝑈 = (𝑠 ∈ (-π[,]π) ↦ ((𝐻‘𝑠) · (𝐾‘𝑠))) & ⊢ (𝜑 → ∃𝑎 ∈ ℝ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐻‘𝑠)) ≤ 𝑎) ⇒ ⊢ (𝜑 → ∃𝑏 ∈ ℝ+ ∀𝑠 ∈ (-π[,]π)(abs‘(𝑈‘𝑠)) ≤ 𝑏) | ||
Theorem | fourierdlem78 46139* | 𝐺 is continuous when restricted on an interval not containing 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝐴 ∈ (-π[,]π)) & ⊢ (𝜑 → 𝐵 ∈ (-π[,]π)) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → ¬ 0 ∈ (𝐴(,)𝐵)) & ⊢ (𝜑 → (𝐹 ↾ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋))) ∈ (((𝐴 + 𝑋)(,)(𝐵 + 𝑋))–cn→ℂ)) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 𝑊 ∈ ℝ) & ⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) & ⊢ 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) & ⊢ 𝑈 = (𝑠 ∈ (-π[,]π) ↦ ((𝐻‘𝑠) · (𝐾‘𝑠))) & ⊢ (𝜑 → 𝑁 ∈ ℝ) & ⊢ 𝑆 = (𝑠 ∈ (-π[,]π) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑠))) & ⊢ 𝐺 = (𝑠 ∈ (-π[,]π) ↦ ((𝑈‘𝑠) · (𝑆‘𝑠))) ⇒ ⊢ (𝜑 → (𝐺 ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℝ)) | ||
Theorem | fourierdlem79 46140* | 𝐸 projects every interval of the partition induced by 𝑆 on 𝐻 into a corresponding interval of the partition induced by 𝑄 on [𝐴, 𝐵]. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝑇 = (𝐵 − 𝐴) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐶 < 𝐷) & ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) & ⊢ 𝑁 = ((♯‘𝐻) − 1) & ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻)) & ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) & ⊢ 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)) & ⊢ 𝑍 = ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) & ⊢ 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < )) ⇒ ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐿‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝑗)))(,)(𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))) | ||
Theorem | fourierdlem80 46141* | The derivative of 𝑂 is bounded on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π)) & ⊢ (𝜑 → ¬ 0 ∈ (𝐴[,]𝐵)) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ 𝑂 = (𝑠 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))) & ⊢ 𝐼 = ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))) & ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ∃𝑤 ∈ ℝ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤) & ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ∃𝑧 ∈ ℝ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧) & ⊢ (𝜑 → 𝑆:(0...𝑁)⟶(𝐴[,]𝐵)) & ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) < (𝑆‘(𝑗 + 1))) & ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵)) & ⊢ (((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑟 ∈ ran 𝑆) → ∃𝑘 ∈ (0..^𝑁)𝑟 ∈ ((𝑆‘𝑘)(,)(𝑆‘(𝑘 + 1)))) & ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝐹 ↾ 𝐼)):𝐼⟶ℝ) & ⊢ 𝑌 = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))) & ⊢ (𝜒 ↔ (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤) ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) ⇒ ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑏) | ||
Theorem | fourierdlem81 46142* | The integral of a piecewise continuous periodic function 𝐹 is unchanged if the domain is shifted by its period 𝑇. In this lemma, 𝑇 is assumed to be strictly positive. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑇 ∈ ℝ+) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ 𝑆 = (𝑖 ∈ (0...𝑀) ↦ ((𝑄‘𝑖) + 𝑇)) & ⊢ (𝜑 → 𝐹:ℝ⟶ℂ) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) & ⊢ 𝐺 = (𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘𝑥)))) & ⊢ 𝐻 = (𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1))) ↦ (𝐺‘(𝑥 − 𝑇))) ⇒ ⊢ (𝜑 → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) | ||
Theorem | fourierdlem82 46143* | Integral by substitution, adding a constant to the function's argument, for a function on an open interval with finite limits ad boundary points. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥)))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ) & ⊢ (𝜑 → (𝐹 ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) & ⊢ (𝜑 → 𝐿 ∈ (𝐹 limℂ 𝐵)) & ⊢ (𝜑 → 𝑅 ∈ (𝐹 limℂ 𝐴)) & ⊢ (𝜑 → 𝑋 ∈ ℝ) ⇒ ⊢ (𝜑 → ∫(𝐴[,]𝐵)(𝐹‘𝑡) d𝑡 = ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡) | ||
Theorem | fourierdlem83 46144* | The fourier partial sum for 𝐹 rewritten as an integral. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ 𝐶 = (-π(,)π) & ⊢ (𝜑 → (𝐹 ↾ 𝐶) ∈ 𝐿1) & ⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ 𝑆 = (𝑚 ∈ ℕ ↦ (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑚)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))))) & ⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑠 ∈ ℝ ↦ if((𝑠 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) · (sin‘(𝑠 / 2))))))) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝑆‘𝑁) = ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥) | ||
Theorem | fourierdlem84 46145* | If 𝐹 is piecewise continuous and 𝐷 is continuous, then 𝐺 is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑋) ∧ (𝑝‘𝑚) = (𝐵 + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) limℂ (𝑉‘𝑖))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) limℂ (𝑉‘(𝑖 + 1)))) & ⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋)) & ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝐷 ∈ (ℝ–cn→ℝ)) & ⊢ 𝐺 = (𝑠 ∈ (𝐴[,]𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) · (𝐷‘𝑠))) ⇒ ⊢ (𝜑 → 𝐺 ∈ 𝐿1) | ||
Theorem | fourierdlem85 46146* | Limit of the function 𝐺 at the lower bounds of the partition intervals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝‘𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝑋 ∈ ran 𝑉) & ⊢ (𝜑 → 𝑌 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) & ⊢ (𝜑 → 𝑊 ∈ ℝ) & ⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) & ⊢ 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) & ⊢ 𝑈 = (𝑠 ∈ (-π[,]π) ↦ ((𝐻‘𝑠) · (𝐾‘𝑠))) & ⊢ (𝜑 → 𝑁 ∈ ℝ) & ⊢ 𝑆 = (𝑠 ∈ (-π[,]π) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑠))) & ⊢ 𝐺 = (𝑠 ∈ (-π[,]π) ↦ ((𝑈‘𝑠) · (𝑆‘𝑠))) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) limℂ (𝑉‘𝑖))) & ⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋)) & ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝐼 = (ℝ D 𝐹) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐼 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℂ) & ⊢ (𝜑 → 𝐸 ∈ ((𝐼 ↾ (𝑋(,)+∞)) limℂ 𝑋)) & ⊢ 𝐴 = ((if((𝑉‘𝑖) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) / (𝑄‘𝑖))) · (𝐾‘(𝑄‘𝑖))) · (𝑆‘(𝑄‘𝑖))) ⇒ ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) | ||
Theorem | fourierdlem86 46147* | Continuity of 𝑂 and its limits with respect to the 𝑆 partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝‘𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) limℂ (𝑉‘𝑖))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) limℂ (𝑉‘(𝑖 + 1)))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π)) & ⊢ (𝜑 → ¬ 0 ∈ (𝐴[,]𝐵)) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ 𝑂 = (𝑠 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) & ⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋)) & ⊢ 𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) & ⊢ 𝑁 = ((♯‘𝑇) − 1) & ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇)) & ⊢ 𝐷 = (((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑈 + 1)), ⦋𝑈 / 𝑖⦌𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) · ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))))) & ⊢ 𝐸 = (((if((𝑆‘𝑗) = (𝑄‘𝑈), ⦋𝑈 / 𝑖⦌𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) · ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2))))) & ⊢ 𝑈 = (℩𝑖 ∈ (0..^𝑀)((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ⇒ ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐷 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) limℂ (𝑆‘(𝑗 + 1))) ∧ 𝐸 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) limℂ (𝑆‘𝑗))) ∧ (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))) | ||
Theorem | fourierdlem87 46148* | The integral of 𝐺 goes uniformly ( with respect to 𝑛) to zero if the measure of the domain of integration goes to zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 𝑊 ∈ ℝ) & ⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) & ⊢ 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) & ⊢ 𝑈 = (𝑠 ∈ (-π[,]π) ↦ ((𝐻‘𝑠) · (𝐾‘𝑠))) & ⊢ 𝑆 = (𝑠 ∈ (-π[,]π) ↦ (sin‘((𝑛 + (1 / 2)) · 𝑠))) & ⊢ 𝐺 = (𝑠 ∈ (-π[,]π) ↦ ((𝑈‘𝑠) · (𝑆‘𝑠))) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐻‘𝑠)) ≤ 𝑥) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐺 ∈ 𝐿1) & ⊢ 𝐷 = ((𝑒 / 3) / 𝑎) & ⊢ (𝜒 ↔ (((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑎 ∈ ℝ+ ∧ ∀𝑛 ∈ ℕ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐺‘𝑠)) ≤ 𝑎) ∧ 𝑢 ∈ dom vol) ∧ (𝑢 ⊆ (-π[,]π) ∧ (vol‘𝑢) ≤ 𝐷)) ∧ 𝑛 ∈ ℕ)) ⇒ ⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → ∃𝑑 ∈ ℝ+ ∀𝑢 ∈ dom vol((𝑢 ⊆ (-π[,]π) ∧ (vol‘𝑢) ≤ 𝑑) → ∀𝑘 ∈ ℕ (abs‘∫𝑢((𝑈‘𝑠) · (sin‘((𝑘 + (1 / 2)) · 𝑠))) d𝑠) < (𝑒 / 2))) | ||
Theorem | fourierdlem88 46149* | Given a piecewise continuous function 𝐹, a continuous function 𝐾 and a continuous function 𝑆, the function 𝐺 is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝‘𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝑋 ∈ ran 𝑉) & ⊢ (𝜑 → 𝑌 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) & ⊢ (𝜑 → 𝑊 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) & ⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) & ⊢ 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) & ⊢ 𝑈 = (𝑠 ∈ (-π[,]π) ↦ ((𝐻‘𝑠) · (𝐾‘𝑠))) & ⊢ (𝜑 → 𝑁 ∈ ℝ) & ⊢ 𝑆 = (𝑠 ∈ (-π[,]π) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑠))) & ⊢ 𝐺 = (𝑠 ∈ (-π[,]π) ↦ ((𝑈‘𝑠) · (𝑆‘𝑠))) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) limℂ (𝑉‘𝑖))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) limℂ (𝑉‘(𝑖 + 1)))) & ⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋)) & ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝐼 = (ℝ D 𝐹) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐼 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℝ) & ⊢ (𝜑 → 𝐶 ∈ ((𝐼 ↾ (-∞(,)𝑋)) limℂ 𝑋)) & ⊢ (𝜑 → 𝐷 ∈ ((𝐼 ↾ (𝑋(,)+∞)) limℂ 𝑋)) ⇒ ⊢ (𝜑 → 𝐺 ∈ 𝐿1) | ||
Theorem | fourierdlem89 46150* | Given a piecewise continuous function and changing the interval and the partition, the limit at the lower bound of each interval of the moved partition is still finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝑇 = (𝐵 − 𝐴) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ (𝜑 → 𝐹:ℝ⟶ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ (𝐶(,)+∞)) & ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) & ⊢ 𝑁 = ((♯‘𝐻) − 1) & ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻)) & ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) & ⊢ 𝑍 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)) & ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁)) & ⊢ 𝑈 = ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1)))) & ⊢ 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝑍‘(𝐸‘𝑥))}, ℝ, < )) & ⊢ 𝑉 = (𝑖 ∈ (0..^𝑀) ↦ 𝑅) ⇒ ⊢ (𝜑 → if((𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽))), (𝑉‘(𝐼‘(𝑆‘𝐽))), (𝐹‘(𝑍‘(𝐸‘(𝑆‘𝐽))))) ∈ ((𝐹 ↾ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1)))) limℂ (𝑆‘𝐽))) | ||
Theorem | fourierdlem90 46151* | Given a piecewise continuous function, it is still continuous with respect to an open interval of the moved partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝑇 = (𝐵 − 𝐴) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ (𝜑 → 𝐹:ℝ⟶ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ (𝐶(,)+∞)) & ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) & ⊢ 𝑁 = ((♯‘𝐻) − 1) & ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻)) & ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) & ⊢ 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)) & ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁)) & ⊢ 𝑈 = ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1)))) & ⊢ 𝐺 = (𝐹 ↾ ((𝐿‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))) & ⊢ 𝑅 = (𝑦 ∈ (((𝐿‘(𝐸‘(𝑆‘𝐽))) + 𝑈)(,)((𝐸‘(𝑆‘(𝐽 + 1))) + 𝑈)) ↦ (𝐺‘(𝑦 − 𝑈))) & ⊢ 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < )) ⇒ ⊢ (𝜑 → (𝐹 ↾ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1)))) ∈ (((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1)))–cn→ℂ)) | ||
Theorem | fourierdlem91 46152* | Given a piecewise continuous function and changing the interval and the partition, the limit at the upper bound of each interval of the moved partition is still finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝑇 = (𝐵 − 𝐴) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ (𝜑 → 𝐹:ℝ⟶ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ (𝐶(,)+∞)) & ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) & ⊢ 𝑁 = ((♯‘𝐻) − 1) & ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻)) & ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) & ⊢ 𝑍 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)) & ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁)) & ⊢ 𝑈 = ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1)))) & ⊢ 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝑍‘(𝐸‘𝑥))}, ℝ, < )) & ⊢ 𝑊 = (𝑖 ∈ (0..^𝑀) ↦ 𝐿) ⇒ ⊢ (𝜑 → if((𝐸‘(𝑆‘(𝐽 + 1))) = (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)), (𝑊‘(𝐼‘(𝑆‘𝐽))), (𝐹‘(𝐸‘(𝑆‘(𝐽 + 1))))) ∈ ((𝐹 ↾ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1)))) limℂ (𝑆‘(𝐽 + 1)))) | ||
Theorem | fourierdlem92 46153* | The integral of a piecewise continuous periodic function 𝐹 is unchanged if the domain is shifted by its period 𝑇. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑇 ∈ ℝ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ 𝑆 = (𝑖 ∈ (0...𝑀) ↦ ((𝑄‘𝑖) + 𝑇)) & ⊢ 𝐻 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝‘𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝐹:ℝ⟶ℂ) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) ⇒ ⊢ (𝜑 → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) | ||
Theorem | fourierdlem93 46154* | Integral by substitution (the domain is shifted by 𝑋) for a piecewise continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝐻 = (𝑖 ∈ (0...𝑀) ↦ ((𝑄‘𝑖) − 𝑋)) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝐹:(-π[,]π)⟶ℂ) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) ⇒ ⊢ (𝜑 → ∫(-π[,]π)(𝐹‘𝑡) d𝑡 = ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑠)) d𝑠) | ||
Theorem | fourierdlem94 46155* | For a piecewise smooth function, the left and the right limits exist at any point. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ 𝑇 = (2 · π) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ 𝑃 = (𝑛 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑛)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑛) = π) ∧ ∀𝑖 ∈ (0..^𝑛)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖)) ≠ ∅) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1))) ≠ ∅) ⇒ ⊢ (𝜑 → (((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋) ≠ ∅ ∧ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋) ≠ ∅)) | ||
Theorem | fourierdlem95 46156* | Algebraic manipulation of integrals, used by other lemmas. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝‘𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝑉) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) limℂ (𝑉‘𝑖))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) limℂ (𝑉‘(𝑖 + 1)))) & ⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) & ⊢ 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) & ⊢ 𝑈 = (𝑠 ∈ (-π[,]π) ↦ ((𝐻‘𝑠) · (𝐾‘𝑠))) & ⊢ 𝑆 = (𝑠 ∈ (-π[,]π) ↦ (sin‘((𝑛 + (1 / 2)) · 𝑠))) & ⊢ 𝐺 = (𝑠 ∈ (-π[,]π) ↦ ((𝑈‘𝑠) · (𝑆‘𝑠))) & ⊢ 𝐼 = (ℝ D 𝐹) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐼 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℝ) & ⊢ (𝜑 → 𝐵 ∈ ((𝐼 ↾ (-∞(,)𝑋)) limℂ 𝑋)) & ⊢ (𝜑 → 𝐶 ∈ ((𝐼 ↾ (𝑋(,)+∞)) limℂ 𝑋)) & ⊢ (𝜑 → 𝑌 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) & ⊢ (𝜑 → 𝑊 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) & ⊢ (𝜑 → 𝐴 ∈ dom vol) & ⊢ (𝜑 → 𝐴 ⊆ ((-π[,]π) ∖ {0})) & ⊢ 𝐸 = (𝑛 ∈ ℕ ↦ (∫𝐴(𝐺‘𝑠) d𝑠 / π)) & ⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑠 ∈ ℝ ↦ if((𝑠 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) · (sin‘(𝑠 / 2))))))) & ⊢ (𝜑 → 𝑂 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑂) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∫𝐴((𝐷‘𝑛)‘𝑠) d𝑠 = (1 / 2)) ⇒ ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐸‘𝑛) + (𝑂 / 2)) = ∫𝐴((𝐹‘(𝑋 + 𝑠)) · ((𝐷‘𝑛)‘𝑠)) d𝑠) | ||
Theorem | fourierdlem96 46157* | limit for 𝐹 at the lower bound of an interval for the moved partition 𝑉. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝑇 = (𝐵 − 𝐴) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ (𝐶(,)+∞)) & ⊢ (𝜑 → 𝐽 ∈ (0..^((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1))) & ⊢ 𝑉 = (℩𝑔𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄}))) ⇒ ⊢ (𝜑 → if(((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘𝐽))) = (𝑄‘((𝑦 ∈ ℝ ↦ sup({𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑦))}, ℝ, < ))‘(𝑉‘𝐽))), ((𝑖 ∈ (0..^𝑀) ↦ 𝑅)‘((𝑦 ∈ ℝ ↦ sup({𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑦))}, ℝ, < ))‘(𝑉‘𝐽))), (𝐹‘((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘𝐽))))) ∈ ((𝐹 ↾ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) limℂ (𝑉‘𝐽))) | ||
Theorem | fourierdlem97 46158* | 𝐹 is continuous on the intervals induced by the moved partition 𝑉. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ 𝐺 = (ℝ D 𝐹) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ 𝑇 = (𝐵 − 𝐴) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ (𝐶(,)+∞)) & ⊢ (𝜑 → 𝐽 ∈ (0..^((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1))) & ⊢ 𝑉 = (℩𝑔𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄}))) & ⊢ 𝐻 = (𝑠 ∈ ℝ ↦ if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0)) ⇒ ⊢ (𝜑 → (𝐺 ↾ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∈ (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))–cn→ℂ)) | ||
Theorem | fourierdlem98 46159* | 𝐹 is continuous on the intervals induced by the moved partition 𝑉. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝑇 = (𝐵 − 𝐴) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ (𝐶(,)+∞)) & ⊢ (𝜑 → 𝐽 ∈ (0..^((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1))) & ⊢ 𝑉 = (℩𝑔𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄}))) ⇒ ⊢ (𝜑 → (𝐹 ↾ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∈ (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))–cn→ℂ)) | ||
Theorem | fourierdlem99 46160* | limit for 𝐹 at the upper bound of an interval for the moved partition 𝑉. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝑇 = (𝐵 − 𝐴) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ (𝐶(,)+∞)) & ⊢ (𝜑 → 𝐽 ∈ (0..^((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1))) & ⊢ 𝑉 = (℩𝑔𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄}))) ⇒ ⊢ (𝜑 → if(((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))) = (𝑄‘(((𝑦 ∈ ℝ ↦ sup({𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑦))}, ℝ, < ))‘(𝑉‘𝐽)) + 1)), ((𝑖 ∈ (0..^𝑀) ↦ 𝐿)‘((𝑦 ∈ ℝ ↦ sup({𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑦))}, ℝ, < ))‘(𝑉‘𝐽))), (𝐹‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))))) ∈ ((𝐹 ↾ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) limℂ (𝑉‘(𝐽 + 1)))) | ||
Theorem | fourierdlem100 46161* | A piecewise continuous function is integrable on any closed interval. This lemma uses local definitions, so that the proof is more readable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝑇 = (𝐵 − 𝐴) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ (𝜑 → 𝐹:ℝ⟶ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ (𝐶(,)+∞)) & ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝑁 = ((♯‘𝐻) − 1) & ⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) & ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻)) & ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) & ⊢ 𝐽 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)) & ⊢ 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐽‘(𝐸‘𝑥))}, ℝ, < )) ⇒ ⊢ (𝜑 → (𝑥 ∈ (𝐶[,]𝐷) ↦ (𝐹‘𝑥)) ∈ 𝐿1) | ||
Theorem | fourierdlem101 46162* | Integral by substitution for a piecewise continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑠 ∈ ℝ ↦ if((𝑠 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) · (sin‘(𝑠 / 2))))))) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝐺 = (𝑡 ∈ (-π[,]π) ↦ ((𝐹‘𝑡) · ((𝐷‘𝑁)‘(𝑡 − 𝑋)))) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝐹:(-π[,]π)⟶ℂ) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) ⇒ ⊢ (𝜑 → ∫(-π[,]π)((𝐹‘𝑡) · ((𝐷‘𝑁)‘(𝑡 − 𝑋))) d𝑡 = ∫((-π − 𝑋)[,](π − 𝑋))((𝐹‘(𝑋 + 𝑠)) · ((𝐷‘𝑁)‘𝑠)) d𝑠) | ||
Theorem | fourierdlem102 46163* | For a piecewise smooth function, the left and the right limits exist at any point. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ 𝑇 = (2 · π) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ 𝐺 = ((ℝ D 𝐹) ↾ (-π(,)π)) & ⊢ (𝜑 → ((-π(,)π) ∖ dom 𝐺) ∈ Fin) & ⊢ (𝜑 → 𝐺 ∈ (dom 𝐺–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ 𝑃 = (𝑛 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑛)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑛) = π) ∧ ∀𝑖 ∈ (0..^𝑛)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇))) & ⊢ 𝐻 = ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) & ⊢ 𝑀 = ((♯‘𝐻) − 1) & ⊢ 𝑄 = (℩𝑔𝑔 Isom < , < ((0...𝑀), 𝐻)) ⇒ ⊢ (𝜑 → (((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋) ≠ ∅ ∧ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋) ≠ ∅)) | ||
Theorem | fourierdlem103 46164* | The half lower part of the integral equal to the fourier partial sum, converges to half the left limit of the original function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝‘𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝑉) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∃𝑤 ∈ ℝ ∀𝑡 ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))(abs‘(𝐹‘𝑡)) ≤ 𝑤) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℝ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∃𝑧 ∈ ℝ ∀𝑡 ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) limℂ (𝑉‘𝑖))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) limℂ (𝑉‘(𝑖 + 1)))) & ⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) & ⊢ 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) & ⊢ 𝑈 = (𝑠 ∈ (-π[,]π) ↦ ((𝐻‘𝑠) · (𝐾‘𝑠))) & ⊢ 𝑆 = (𝑠 ∈ (-π[,]π) ↦ (sin‘((𝑛 + (1 / 2)) · 𝑠))) & ⊢ 𝐺 = (𝑠 ∈ (-π[,]π) ↦ ((𝑈‘𝑠) · (𝑆‘𝑠))) & ⊢ 𝑍 = (𝑚 ∈ ℕ ↦ ∫(-π(,)0)((𝐹‘(𝑋 + 𝑠)) · ((𝐷‘𝑚)‘𝑠)) d𝑠) & ⊢ 𝐸 = (𝑛 ∈ ℕ ↦ (∫(-π(,)0)(𝐺‘𝑠) d𝑠 / π)) & ⊢ (𝜑 → 𝑌 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) & ⊢ (𝜑 → 𝑊 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) & ⊢ (𝜑 → 𝐴 ∈ (((ℝ D 𝐹) ↾ (-∞(,)𝑋)) limℂ 𝑋)) & ⊢ (𝜑 → 𝐵 ∈ (((ℝ D 𝐹) ↾ (𝑋(,)+∞)) limℂ 𝑋)) & ⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑠 ∈ ℝ ↦ if((𝑠 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) · (sin‘(𝑠 / 2))))))) & ⊢ 𝑂 = (𝑈 ↾ (-π[,]𝑑)) & ⊢ 𝑇 = ({-π, 𝑑} ∪ (ran 𝑄 ∩ (-π(,)𝑑))) & ⊢ 𝑁 = ((♯‘𝑇) − 1) & ⊢ 𝐽 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇)) & ⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋)) & ⊢ 𝐶 = (℩𝑙 ∈ (0..^𝑀)((𝐽‘𝑘)(,)(𝐽‘(𝑘 + 1))) ⊆ ((𝑄‘𝑙)(,)(𝑄‘(𝑙 + 1)))) & ⊢ (𝜒 ↔ (((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑑 ∈ (-π(,)0)) ∧ 𝑘 ∈ ℕ) ∧ (abs‘∫(𝑑(,)0)((𝑈‘𝑠) · (sin‘((𝑘 + (1 / 2)) · 𝑠))) d𝑠) < (𝑒 / 2)) ∧ (abs‘∫(-π(,)𝑑)((𝑈‘𝑠) · (sin‘((𝑘 + (1 / 2)) · 𝑠))) d𝑠) < (𝑒 / 2))) ⇒ ⊢ (𝜑 → 𝑍 ⇝ (𝑊 / 2)) | ||
Theorem | fourierdlem104 46165* | The half upper part of the integral equal to the fourier partial sum, converges to half the right limit of the original function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝‘𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝑉) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∃𝑤 ∈ ℝ ∀𝑡 ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))(abs‘(𝐹‘𝑡)) ≤ 𝑤) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℝ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∃𝑧 ∈ ℝ ∀𝑡 ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) limℂ (𝑉‘𝑖))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) limℂ (𝑉‘(𝑖 + 1)))) & ⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) & ⊢ 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) & ⊢ 𝑈 = (𝑠 ∈ (-π[,]π) ↦ ((𝐻‘𝑠) · (𝐾‘𝑠))) & ⊢ 𝑆 = (𝑠 ∈ (-π[,]π) ↦ (sin‘((𝑛 + (1 / 2)) · 𝑠))) & ⊢ 𝐺 = (𝑠 ∈ (-π[,]π) ↦ ((𝑈‘𝑠) · (𝑆‘𝑠))) & ⊢ 𝑍 = (𝑚 ∈ ℕ ↦ ∫(0(,)π)((𝐹‘(𝑋 + 𝑠)) · ((𝐷‘𝑚)‘𝑠)) d𝑠) & ⊢ 𝐸 = (𝑛 ∈ ℕ ↦ (∫(0(,)π)(𝐺‘𝑠) d𝑠 / π)) & ⊢ (𝜑 → 𝑌 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) & ⊢ (𝜑 → 𝑊 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) & ⊢ (𝜑 → 𝐴 ∈ (((ℝ D 𝐹) ↾ (-∞(,)𝑋)) limℂ 𝑋)) & ⊢ (𝜑 → 𝐵 ∈ (((ℝ D 𝐹) ↾ (𝑋(,)+∞)) limℂ 𝑋)) & ⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑠 ∈ ℝ ↦ if((𝑠 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) · (sin‘(𝑠 / 2))))))) & ⊢ 𝑂 = (𝑈 ↾ (𝑑[,]π)) & ⊢ 𝑇 = ({𝑑, π} ∪ (ran 𝑄 ∩ (𝑑(,)π))) & ⊢ 𝑁 = ((♯‘𝑇) − 1) & ⊢ 𝐽 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇)) & ⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋)) & ⊢ 𝐶 = (℩𝑙 ∈ (0..^𝑀)((𝐽‘𝑘)(,)(𝐽‘(𝑘 + 1))) ⊆ ((𝑄‘𝑙)(,)(𝑄‘(𝑙 + 1)))) & ⊢ (𝜒 ↔ (((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑑 ∈ (0(,)π)) ∧ 𝑘 ∈ ℕ) ∧ (abs‘∫(0(,)𝑑)((𝑈‘𝑠) · (sin‘((𝑘 + (1 / 2)) · 𝑠))) d𝑠) < (𝑒 / 2)) ∧ (abs‘∫(𝑑(,)π)((𝑈‘𝑠) · (sin‘((𝑘 + (1 / 2)) · 𝑠))) d𝑠) < (𝑒 / 2))) ⇒ ⊢ (𝜑 → 𝑍 ⇝ (𝑌 / 2)) | ||
Theorem | fourierdlem105 46166* | A piecewise continuous function is integrable on any closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝑇 = (𝐵 − 𝐴) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ (𝜑 → 𝐹:ℝ⟶ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ (𝐶(,)+∞)) ⇒ ⊢ (𝜑 → (𝑥 ∈ (𝐶[,]𝐷) ↦ (𝐹‘𝑥)) ∈ 𝐿1) | ||
Theorem | fourierdlem106 46167* | For a piecewise smooth function, the left and the right limits exist at any point. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ 𝑇 = (2 · π) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ 𝐺 = ((ℝ D 𝐹) ↾ (-π(,)π)) & ⊢ (𝜑 → ((-π(,)π) ∖ dom 𝐺) ∈ Fin) & ⊢ (𝜑 → 𝐺 ∈ (dom 𝐺–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅) & ⊢ (𝜑 → 𝑋 ∈ ℝ) ⇒ ⊢ (𝜑 → (((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋) ≠ ∅ ∧ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋) ≠ ∅)) | ||
Theorem | fourierdlem107 46168* | The integral of a piecewise continuous periodic function 𝐹 is unchanged if the domain is shifted by any positive value 𝑋. This lemma generalizes fourierdlem92 46153 where the integral was shifted by the exact period. This lemma uses local definitions, so that the proof is more readable. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ 𝑇 = (𝐵 − 𝐴) & ⊢ (𝜑 → 𝑋 ∈ ℝ+) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ (𝜑 → 𝐹:ℝ⟶ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) & ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 − 𝑋) ∧ (𝑝‘𝑚) = 𝐴) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝐻 = ({(𝐴 − 𝑋), 𝐴} ∪ {𝑦 ∈ ((𝐴 − 𝑋)[,]𝐴) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) & ⊢ 𝑁 = ((♯‘𝐻) − 1) & ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻)) & ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) & ⊢ 𝑍 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)) & ⊢ 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝑍‘(𝐸‘𝑥))}, ℝ, < )) ⇒ ⊢ (𝜑 → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) | ||
Theorem | fourierdlem108 46169* | The integral of a piecewise continuous periodic function 𝐹 is unchanged if the domain is shifted by any positive value 𝑋. This lemma generalizes fourierdlem92 46153 where the integral was shifted by the exact period. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ 𝑇 = (𝐵 − 𝐴) & ⊢ (𝜑 → 𝑋 ∈ ℝ+) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ (𝜑 → 𝐹:ℝ⟶ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) ⇒ ⊢ (𝜑 → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) | ||
Theorem | fourierdlem109 46170* | The integral of a piecewise continuous periodic function 𝐹 is unchanged if the domain is shifted by any value 𝑋. This lemma generalizes fourierdlem92 46153 where the integral was shifted by the exact period. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ 𝑇 = (𝐵 − 𝐴) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ (𝜑 → 𝐹:ℝ⟶ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) & ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 − 𝑋) ∧ (𝑝‘𝑚) = (𝐵 − 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝐻 = ({(𝐴 − 𝑋), (𝐵 − 𝑋)} ∪ {𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) & ⊢ 𝑁 = ((♯‘𝐻) − 1) & ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻)) & ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) & ⊢ 𝐽 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)) & ⊢ 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) ≤ (𝐽‘(𝐸‘𝑥))}, ℝ, < )) ⇒ ⊢ (𝜑 → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) | ||
Theorem | fourierdlem110 46171* | The integral of a piecewise continuous periodic function 𝐹 is unchanged if the domain is shifted by any value 𝑋. This lemma generalizes fourierdlem92 46153 where the integral was shifted by the exact period. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ 𝑇 = (𝐵 − 𝐴) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ (𝜑 → 𝐹:ℝ⟶ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) ⇒ ⊢ (𝜑 → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) | ||
Theorem | fourierdlem111 46172* | The fourier partial sum for 𝐹 is the sum of two integrals, with the same integrand involving 𝐹 and the Dirichlet Kernel 𝐷, but on two opposite intervals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫(-π(,)π)((𝐹‘𝑡) · (cos‘(𝑛 · 𝑡))) d𝑡 / π)) & ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑡) · (sin‘(𝑛 · 𝑡))) d𝑡 / π)) & ⊢ 𝑆 = (𝑚 ∈ ℕ ↦ (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑚)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))))) & ⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2))))))) & ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ ((𝐹‘(𝑋 + 𝑥)) · ((𝐷‘𝑛)‘𝑥))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) & ⊢ 𝑇 = (2 · π) & ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (-π − 𝑋) ∧ (𝑝‘𝑚) = (π − 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝑊 = (𝑖 ∈ (0...𝑀) ↦ ((𝑄‘𝑖) − 𝑋)) ⇒ ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑆‘𝑛) = (∫(-π(,)0)((𝐹‘(𝑋 + 𝑠)) · ((𝐷‘𝑛)‘𝑠)) d𝑠 + ∫(0(,)π)((𝐹‘(𝑋 + 𝑠)) · ((𝐷‘𝑛)‘𝑠)) d𝑠)) | ||
Theorem | fourierdlem112 46173* | Here abbreviations (local definitions) are introduced to prove the fourier 46180 theorem. (𝑍‘𝑚) is the mth partial sum of the fourier series. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ 𝐷 = (𝑚 ∈ ℕ ↦ (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑚) + 1) / (2 · π)), ((sin‘((𝑚 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2))))))) & ⊢ 𝑃 = (𝑛 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑛)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑛) = π) ∧ ∀𝑖 ∈ (0..^𝑛)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ 𝑁 = ((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1) & ⊢ 𝑉 = (℩𝑓𝑓 Isom < , < ((0...𝑁), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ∈ ran 𝑉) & ⊢ 𝑇 = (2 · π) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐶 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑈 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ (𝜑 → 𝐸 ∈ (((ℝ D 𝐹) ↾ (-∞(,)𝑋)) limℂ 𝑋)) & ⊢ (𝜑 → 𝐼 ∈ (((ℝ D 𝐹) ↾ (𝑋(,)+∞)) limℂ 𝑋)) & ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) & ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) & ⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ 𝑍 = (𝑚 ∈ ℕ ↦ (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑚)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))))) & ⊢ 𝑆 = (𝑛 ∈ ℕ ↦ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) & ⊢ (𝜑 → ∃𝑤 ∈ ℝ ∀𝑡 ∈ ℝ (abs‘(𝐹‘𝑡)) ≤ 𝑤) & ⊢ (𝜑 → ∃𝑧 ∈ ℝ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) & ⊢ (𝜑 → 𝑋 ∈ ℝ) ⇒ ⊢ (𝜑 → (seq1( + , 𝑆) ⇝ (((𝐿 + 𝑅) / 2) − ((𝐴‘0) / 2)) ∧ (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝐿 + 𝑅) / 2))) | ||
Theorem | fourierdlem113 46174* | Fourier series convergence for periodic, piecewise smooth functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ 𝑇 = (2 · π) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) & ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) & ⊢ 𝑃 = (𝑛 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑛)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑛) = π) ∧ ∀𝑖 ∈ (0..^𝑛)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖)) ≠ ∅) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1))) ≠ ∅) & ⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ 𝑆 = (𝑛 ∈ ℕ ↦ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) & ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇))) & ⊢ (𝜑 → (𝐸‘𝑋) ∈ ran 𝑄) ⇒ ⊢ (𝜑 → (seq1( + , 𝑆) ⇝ (((𝐿 + 𝑅) / 2) − ((𝐴‘0) / 2)) ∧ (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝐿 + 𝑅) / 2))) | ||
Theorem | fourierdlem114 46175* | Fourier series convergence for periodic, piecewise smooth functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ 𝑇 = (2 · π) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ 𝐺 = ((ℝ D 𝐹) ↾ (-π(,)π)) & ⊢ (𝜑 → ((-π(,)π) ∖ dom 𝐺) ∈ Fin) & ⊢ (𝜑 → 𝐺 ∈ (dom 𝐺–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) & ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) & ⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ 𝑆 = (𝑛 ∈ ℕ ↦ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) & ⊢ 𝑃 = (𝑛 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑛)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑛) = π) ∧ ∀𝑖 ∈ (0..^𝑛)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) & ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇))) & ⊢ 𝐻 = ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) & ⊢ 𝑀 = ((♯‘𝐻) − 1) & ⊢ 𝑄 = (℩𝑔𝑔 Isom < , < ((0...𝑀), 𝐻)) ⇒ ⊢ (𝜑 → (seq1( + , 𝑆) ⇝ (((𝐿 + 𝑅) / 2) − ((𝐴‘0) / 2)) ∧ (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝐿 + 𝑅) / 2))) | ||
Theorem | fourierdlem115 46176* | Fourier serier convergence, for piecewise smooth functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ 𝑇 = (2 · π) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ 𝐺 = ((ℝ D 𝐹) ↾ (-π(,)π)) & ⊢ (𝜑 → ((-π(,)π) ∖ dom 𝐺) ∈ Fin) & ⊢ (𝜑 → 𝐺 ∈ (dom 𝐺–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) & ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) & ⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ 𝑆 = (𝑘 ∈ ℕ ↦ (((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋))))) ⇒ ⊢ (𝜑 → (seq1( + , 𝑆) ⇝ (((𝐿 + 𝑅) / 2) − ((𝐴‘0) / 2)) ∧ (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝐿 + 𝑅) / 2))) | ||
Theorem | fourierd 46177* | Fourier series convergence for periodic, piecewise smooth functions. The series converges to the average value of the left and the right limit of the function. Thus, if the function is continuous at a given point, the series converges exactly to the function value, see fouriercnp 46181. Notice that for a piecewise smooth function, the left and right limits always exist, see fourier2 46182 for an alternative form of the theorem that makes this fact explicit. When the first derivative is continuous, a simpler version of the theorem can be stated, see fouriercn 46187. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ 𝑇 = (2 · π) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ 𝐺 = ((ℝ D 𝐹) ↾ (-π(,)π)) & ⊢ (𝜑 → ((-π(,)π) ∖ dom 𝐺) ∈ Fin) & ⊢ (𝜑 → 𝐺 ∈ (dom 𝐺–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) & ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) & ⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) ⇒ ⊢ (𝜑 → (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝐿 + 𝑅) / 2)) | ||
Theorem | fourierclimd 46178* | Fourier series convergence, for piecewise smooth functions. See fourierd 46177 for the analogous Σ equation. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ 𝑇 = (2 · π) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ 𝐺 = ((ℝ D 𝐹) ↾ (-π(,)π)) & ⊢ (𝜑 → ((-π(,)π) ∖ dom 𝐺) ∈ Fin) & ⊢ (𝜑 → 𝐺 ∈ (dom 𝐺–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)) & ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)) & ⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ 𝑆 = (𝑛 ∈ ℕ ↦ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) ⇒ ⊢ (𝜑 → seq1( + , 𝑆) ⇝ (((𝐿 + 𝑅) / 2) − ((𝐴‘0) / 2))) | ||
Theorem | fourierclim 46179* | Fourier series convergence, for piecewise smooth functions. See fourier 46180 for the analogous Σ equation. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹:ℝ⟶ℝ & ⊢ 𝑇 = (2 · π) & ⊢ (𝑥 ∈ ℝ → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ 𝐺 = ((ℝ D 𝐹) ↾ (-π(,)π)) & ⊢ ((-π(,)π) ∖ dom 𝐺) ∈ Fin & ⊢ 𝐺 ∈ (dom 𝐺–cn→ℂ) & ⊢ (𝑥 ∈ ((-π[,)π) ∖ dom 𝐺) → ((𝐺 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅) & ⊢ (𝑥 ∈ ((-π(,]π) ∖ dom 𝐺) → ((𝐺 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅) & ⊢ 𝑋 ∈ ℝ & ⊢ 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋) & ⊢ 𝑅 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋) & ⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ 𝑆 = (𝑛 ∈ ℕ ↦ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) ⇒ ⊢ seq1( + , 𝑆) ⇝ (((𝐿 + 𝑅) / 2) − ((𝐴‘0) / 2)) | ||
Theorem | fourier 46180* | Fourier series convergence for periodic, piecewise smooth functions. The series converges to the average value of the left and the right limit of the function. Thus, if the function is continuous at a given point, the series converges exactly to the function value, see fouriercnp 46181. Notice that for a piecewise smooth function, the left and right limits always exist, see fourier2 46182 for an alternative form of the theorem that makes this fact explicit. When the first derivative is continuous, a simpler version of the theorem can be stated, see fouriercn 46187. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐹:ℝ⟶ℝ & ⊢ 𝑇 = (2 · π) & ⊢ (𝑥 ∈ ℝ → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ 𝐺 = ((ℝ D 𝐹) ↾ (-π(,)π)) & ⊢ ((-π(,)π) ∖ dom 𝐺) ∈ Fin & ⊢ 𝐺 ∈ (dom 𝐺–cn→ℂ) & ⊢ (𝑥 ∈ ((-π[,)π) ∖ dom 𝐺) → ((𝐺 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅) & ⊢ (𝑥 ∈ ((-π(,]π) ∖ dom 𝐺) → ((𝐺 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅) & ⊢ 𝑋 ∈ ℝ & ⊢ 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋) & ⊢ 𝑅 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋) & ⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) ⇒ ⊢ (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝐿 + 𝑅) / 2) | ||
Theorem | fouriercnp 46181* | If 𝐹 is continuous at the point 𝑋, then its Fourier series at 𝑋, converges to (𝐹‘𝑋). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ 𝑇 = (2 · π) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ 𝐺 = ((ℝ D 𝐹) ↾ (-π(,)π)) & ⊢ (𝜑 → ((-π(,)π) ∖ dom 𝐺) ∈ Fin) & ⊢ (𝜑 → 𝐺 ∈ (dom 𝐺–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅) & ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ (𝜑 → 𝐹 ∈ ((𝐽 CnP 𝐽)‘𝑋)) & ⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) ⇒ ⊢ (𝜑 → (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = (𝐹‘𝑋)) | ||
Theorem | fourier2 46182* | Fourier series convergence, for a piecewise smooth function. Here it is also proven the existence of the left and right limits of 𝐹 at any given point 𝑋. See fourierd 46177 for a comparison. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ 𝑇 = (2 · π) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ 𝐺 = ((ℝ D 𝐹) ↾ (-π(,)π)) & ⊢ (𝜑 → ((-π(,)π) ∖ dom 𝐺) ∈ Fin) & ⊢ (𝜑 → 𝐺 ∈ (dom 𝐺–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) ⇒ ⊢ (𝜑 → ∃𝑙 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋)∃𝑟 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋)(((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝑙 + 𝑟) / 2)) | ||
Theorem | sqwvfoura 46183* | Fourier coefficients for the square wave function. Since the square function is an odd function, there is no contribution from the 𝐴 coefficients. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝑇 = (2 · π) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ if((𝑥 mod 𝑇) < π, 1, -1)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 / π) = 0) | ||
Theorem | sqwvfourb 46184* | Fourier series 𝐵 coefficients for the square wave function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝑇 = (2 · π) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ if((𝑥 mod 𝑇) < π, 1, -1)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑁 · 𝑥))) d𝑥 / π) = if(2 ∥ 𝑁, 0, (4 / (𝑁 · π)))) | ||
Theorem | fourierswlem 46185* | The Fourier series for the square wave 𝐹 converges to 𝑌, a simpler expression for this special case. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝑇 = (2 · π) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ if((𝑥 mod 𝑇) < π, 1, -1)) & ⊢ 𝑋 ∈ ℝ & ⊢ 𝑌 = if((𝑋 mod π) = 0, 0, (𝐹‘𝑋)) ⇒ ⊢ 𝑌 = ((if((𝑋 mod 𝑇) ∈ (0(,]π), 1, -1) + (𝐹‘𝑋)) / 2) | ||
Theorem | fouriersw 46186* | Fourier series convergence, for the square wave function. Where 𝐹 is discontinuous, the series converges to 0, the average value of the left and the right limits. Notice that 𝐹 is an odd function and its Fourier expansion has only sine terms (coefficients for cosine terms are zero). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝑇 = (2 · π) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ if((𝑥 mod 𝑇) < π, 1, -1)) & ⊢ 𝑋 ∈ ℝ & ⊢ 𝑆 = (𝑛 ∈ ℕ ↦ ((sin‘(((2 · 𝑛) − 1) · 𝑋)) / ((2 · 𝑛) − 1))) & ⊢ 𝑌 = if((𝑋 mod π) = 0, 0, (𝐹‘𝑋)) ⇒ ⊢ (((4 / π) · Σ𝑘 ∈ ℕ ((sin‘(((2 · 𝑘) − 1) · 𝑋)) / ((2 · 𝑘) − 1))) = 𝑌 ∧ seq1( + , 𝑆) ⇝ ((π / 4) · 𝑌)) | ||
Theorem | fouriercn 46187* | If the derivative of 𝐹 is continuous, then the Fourier series for 𝐹 converges to 𝐹 everywhere and the hypothesis are simpler than those for the more general case of a piecewise smooth function (see fourierd 46177 for a comparison). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) & ⊢ 𝑇 = (2 · π) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) & ⊢ (𝜑 → (ℝ D 𝐹) ∈ (ℝ–cn→ℂ)) & ⊢ 𝐺 = ((ℝ D 𝐹) ↾ (-π(,)π)) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) & ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) ⇒ ⊢ (𝜑 → (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = (𝐹‘𝑋)) | ||
Theorem | elaa2lem 46188* | Elementhood in the set of nonzero algebraic numbers. ' Only if ' part of elaa2 46189. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Revised by AV, 1-Oct-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝔸) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐺 ∈ (Poly‘ℤ)) & ⊢ (𝜑 → 𝐺 ≠ 0𝑝) & ⊢ (𝜑 → (𝐺‘𝐴) = 0) & ⊢ 𝑀 = inf({𝑛 ∈ ℕ0 ∣ ((coeff‘𝐺)‘𝑛) ≠ 0}, ℝ, < ) & ⊢ 𝐼 = (𝑘 ∈ ℕ0 ↦ ((coeff‘𝐺)‘(𝑘 + 𝑀))) & ⊢ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...((deg‘𝐺) − 𝑀))((𝐼‘𝑘) · (𝑧↑𝑘))) ⇒ ⊢ (𝜑 → ∃𝑓 ∈ (Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0)) | ||
Theorem | elaa2 46189* | Elementhood in the set of nonzero algebraic numbers: when 𝐴 is nonzero, the polynomial 𝑓 can be chosen with a nonzero constant term. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Proof shortened by AV, 1-Oct-2020.) |
⊢ (𝐴 ∈ (𝔸 ∖ {0}) ↔ (𝐴 ∈ ℂ ∧ ∃𝑓 ∈ (Poly‘ℤ)(((coeff‘𝑓)‘0) ≠ 0 ∧ (𝑓‘𝐴) = 0))) | ||
Theorem | etransclem1 46190* | 𝐻 is a function. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑋 ⊆ ℂ) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) & ⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) ⇒ ⊢ (𝜑 → (𝐻‘𝐽):𝑋⟶ℂ) | ||
Theorem | etransclem2 46191* | Derivative of 𝐺. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝐹:ℝ⟶ℂ) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑅 + 1))) → ((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ) & ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥)) ⇒ ⊢ (𝜑 → (ℝ D 𝐺) = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥))) | ||
Theorem | etransclem3 46192 | The given if term is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝐶:(0...𝑀)⟶(0...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) & ⊢ (𝜑 → 𝐾 ∈ ℤ) ⇒ ⊢ (𝜑 → if(𝑃 < (𝐶‘𝐽), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝐽)))) · ((𝐾 − 𝐽)↑(𝑃 − (𝐶‘𝐽))))) ∈ ℤ) | ||
Theorem | etransclem4 46193* | 𝐹 expressed as a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) & ⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) & ⊢ 𝐸 = (𝑥 ∈ 𝐴 ↦ ∏𝑗 ∈ (0...𝑀)((𝐻‘𝑗)‘𝑥)) ⇒ ⊢ (𝜑 → 𝐹 = 𝐸) | ||
Theorem | etransclem5 46194* | A change of bound variable, often used in proofs for etransc 46238. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) = (𝑘 ∈ (0...𝑀) ↦ (𝑦 ∈ 𝑋 ↦ ((𝑦 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))) | ||
Theorem | etransclem6 46195* | A change of bound variable, often used in proofs for etransc 46238. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑦 − 𝑘)↑𝑃))) | ||
Theorem | etransclem7 46196* | The given product is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝐶:(0...𝑀)⟶(0...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) ⇒ ⊢ (𝜑 → ∏𝑗 ∈ (1...𝑀)if(𝑃 < (𝐶‘𝑗), 0, (((!‘𝑃) / (!‘(𝑃 − (𝐶‘𝑗)))) · ((𝐽 − 𝑗)↑(𝑃 − (𝐶‘𝑗))))) ∈ ℤ) | ||
Theorem | etransclem8 46197* | 𝐹 is a function. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑋 ⊆ ℂ) & ⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) ⇒ ⊢ (𝜑 → 𝐹:𝑋⟶ℂ) | ||
Theorem | etransclem9 46198 | If 𝐾 divides 𝑁 but 𝐾 does not divide 𝑀 then 𝑀 + 𝑁 cannot be zero. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ≠ 0) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → ¬ 𝐾 ∥ 𝑀) & ⊢ (𝜑 → 𝐾 ∥ 𝑁) ⇒ ⊢ (𝜑 → (𝑀 + 𝑁) ≠ 0) | ||
Theorem | etransclem10 46199 | The given if term is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑃 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝐶:(0...𝑀)⟶(0...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ ℤ) ⇒ ⊢ (𝜑 → if((𝑃 − 1) < (𝐶‘0), 0, (((!‘(𝑃 − 1)) / (!‘((𝑃 − 1) − (𝐶‘0)))) · (𝐽↑((𝑃 − 1) − (𝐶‘0))))) ∈ ℤ) | ||
Theorem | etransclem11 46200* | A change of bound variable, often used in proofs for etransc 46238. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) = (𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |