Bochner

Results named in Tau Ceti's TauCeti.Analysis.Bochner modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremThe Bochner–Khinchin theorem#

A function F on a finite-dimensional real inner-product space is continuous, positive definite and normalized by F 0 = 1 if and only if it is the characteristic function of a unique Borel probability measure.

TauCeti.bochner_charFun_probabilityMeasure.{u_1} {V : Type u_1} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (F : V → ℂ) :
  Continuous F ∧ TauCeti.IsPositiveDefiniteSub F ∧ F 0 = 1 ↔
    ∃! μ, MeasureTheory.IsProbabilityMeasure μ ∧ MeasureTheory.charFun μ = F
Lean

Formalized in Tau Ceti as TauCeti.bochner_charFun_probabilityMeasure.

Sources
LeanTauCeti.bochner_charFun_probabilityMeasure
Uses 1
Proof usesBochner's theorem

TheoremHerglotz's theorem#

A positive-definite function φ on ℤ is the moment sequence φ n = ∫ zⁿ dμ(z) of a finite positive measure μ on the unit circle.

TauCeti.exists_isFiniteMeasure_integral_zpow_eq (φ : ℤ → ℂ) (hφ : TauCeti.IsPositiveDefiniteSub φ) :
  ∃ μ, MeasureTheory.IsFiniteMeasure μ ∧ ∀ (n : ℤ), φ n = ∫ (z : Circle), ↑z ^ n ∂μ
Lean

Formalized in Tau Ceti as TauCeti.exists_isFiniteMeasure_integral_zpow_eq.

Other forms

Herglotz's theorem, as a characterization. Formalized in Tau Ceti as TauCeti.isPositiveDefiniteSub_iff_exists_isFiniteMeasure_integral_zpow_eq.

TauCeti.isPositiveDefiniteSub_iff_exists_isFiniteMeasure_integral_zpow_eq (φ : ℤ → ℂ) :
  TauCeti.IsPositiveDefiniteSub φ ↔
    ∃ μ, MeasureTheory.IsFiniteMeasure μ ∧ ∀ (n : ℤ), φ n = ∫ (z : Circle), ↑z ^ n ∂μ
Sources
LeanTauCeti.exists_isFiniteMeasure_integral_zpow_eq · TauCeti.isPositiveDefiniteSub_iff_exists_isFiniteMeasure_integral_zpow_eq
Uses 1
Proof usesProkhorov's theorem for finite measures

TheoremThe inversion theorem#

A finite measure on ℝ with integrable characteristic function φ has the bounded continuous density x ↦ (2π)⁻¹ * Re ∫ t, exp (-i t x) * φ(t) dt with respect to Lebesgue measure.

MeasureTheory.Measure.eq_withDensity_charFunDensity {μ : MeasureTheory.Measure ℝ}
  [MeasureTheory.IsFiniteMeasure μ]
  (h : MeasureTheory.Integrable (MeasureTheory.charFun μ) MeasureTheory.volume) :
  μ = MeasureTheory.volume.withDensity fun x => ENNReal.ofReal (μ.charFunDensity x)
Lean

Formalized in Tau Ceti as MeasureTheory.Measure.eq_withDensity_charFunDensity.

Sources
LeanMeasureTheory.Measure.eq_withDensity_charFunDensity
Uses 1
Proof usesUniqueness half of Bochner's theorem

TheoremUniqueness half of Bochner's theorem#

Two finite Borel measures with the same Fourier-convention transform coincide; this is Mathlib's characteristic-function uniqueness theorem, transported through the -2π rescaling. Stated on any complete second-countable real inner-product space; no finite-dimensionality is needed.

TauCeti.Measure.ext_of_forall_integral_fourierAtom_eq.{u_3} {W : Type u_3} [NormedAddCommGroup W]
  [InnerProductSpace ℝ W] [MeasurableSpace W] [BorelSpace W] [SecondCountableTopology W]
  [CompleteSpace W] {μ ν : MeasureTheory.Measure W} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν]
  (h : ∀ (v : W), ∫ (q : W), TauCeti.fourierAtom v q ∂μ = ∫ (q : W), TauCeti.fourierAtom v q ∂ν) :
  μ = ν
Lean

Formalized in Tau Ceti as TauCeti.Measure.ext_of_forall_integral_fourierAtom_eq.

Sources
LeanTauCeti.Measure.ext_of_forall_integral_fourierAtom_eq
Used by 3
Used byThe inversion theorem · Bochner's theorem · The Berg--Christensen--Ressel representation theorem (Berg--Christensen--Ressel 4.1.13)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.