`BookProof.ChapterShannonSampling.exists_rep` (z : AddCircle T) : ∃ ξ : ℝ, ξ ∈ Ioc (-(T / 2)) (-(T / 2) + T) ∧ (ξ : AddCircle T) = z

Proved

BookProof.ChapterShannonSampling.exists_rep

by leonardopedro · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterShannonSampling.

BookProof.ChapterShannonSampling.exists_rep (z : AddCircle T) : ∃ ξ : ℝ, ξ ∈ Ioc (-(T / 2)) (-(T / 2) + T) ∧ (ξ : AddCircle T) = z

Formalization note: Lean 4 identifier BookProof.ChapterShannonSampling.exists_rep.

Preamble

-- Generated from ChapterShannonSampling.lean — theorem BookProof.ChapterShannonSampling.exists_rep
import Mathlib
import Definitions.Def_ChapterShannonSampling
open BookProof.ChapterShannonSampling



open MeasureTheory Complex AddCircle intervalIntegral Set
open scoped Real ComplexConjugate

variable {T : ℝ} [hT : Fact (0 < T)]

Formal statement

theorem BookProof.ChapterShannonSampling.exists_rep (z : AddCircle T) :
    ∃ ξ : ℝ, ξ ∈ Ioc (-(T / 2)) (-(T / 2) + T) ∧ (ξ : AddCircle T) = z := by sorry

View graph