One-parameter semigroups, completely monotone and positive-definite functions, and Bochner-type representations

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

TheoremHille--Yosida characterization#

An unbounded operator is the generator of a strongly continuous semigroup with growth bound (omega, M) if and only if 1 ≤ M, its domain is dense, the half-line (omega, ∞) lies in its resolvent set, and its resolvent powers satisfy the sharp Hille--Yosida estimates.

TauCeti.Semigroups.hilleYosida_generation_iff.{u_1} {X : Type u_1} [NormedAddCommGroup X]
  [NormedSpace ℝ X] [CompleteSpace X] (A : X →ₗ.[ℝ] X) (M omega : ℝ) :
  (∃ S, S.generator = A ∧ S.HasGrowthBound omega M) ↔
    1 ≤ M ∧
      Dense ↑A.domain ∧
        (∀ (lambda : ℝ), omega < lambda → lambda ∈ A.resolventSet) ∧
          ∀ (n : ℕ),
            1 ≤ n →
              ∀ (lambda : ℝ), omega < lambda → ‖A.resolvent lambda ^ n‖ ≤ M / (lambda - omega) ^ n
Informally uses
Lean

Formalized in Tau Ceti as TauCeti.Semigroups.hilleYosida_generation_iff.

Sources
LeanTauCeti.Semigroups.hilleYosida_generation_iff
Uses 1 · Used by 1
Proof usesSharp Hille--Yosida power bound for the generator resolvent
Used byHille--Yosida for contraction semigroups

TheoremHille--Yosida for contraction semigroups#

An unbounded operator A on a real Banach space generates a strongly continuous contraction semigroup if and only if its domain is dense, every lambda > 0 lies in its resolvent set, and ‖R(lambda, A)‖ ≤ 1 / lambda for every lambda > 0.

TauCeti.Semigroups.exists_contractionSemigroup_generator_eq_iff_forall_norm_resolvent_le.{u_1}
  {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →ₗ.[ℝ] X) :
  (∃ S, S.generator = A) ↔
    Dense ↑A.domain ∧
      (∀ (lambda : ℝ), 0 < lambda → lambda ∈ A.resolventSet) ∧
        ∀ (lambda : ℝ), 0 < lambda → ‖A.resolvent lambda‖ ≤ lambda⁻¹
Lean

Formalized in Tau Ceti as TauCeti.Semigroups.exists_contractionSemigroup_generator_eq_iff_forall_norm_resolvent_le.

Other forms

Hille--Yosida for quasi-contraction semigroups. Formalized in Tau Ceti as TauCeti.Semigroups.exists_generator_eq_and_hasGrowthBound_one_iff_forall_norm_resolvent_le.

TauCeti.Semigroups.exists_generator_eq_and_hasGrowthBound_one_iff_forall_norm_resolvent_le.{u_1}
  {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →ₗ.[ℝ] X)
  (omega : ℝ) :
  (∃ S, S.generator = A ∧ S.HasGrowthBound omega 1) ↔
    Dense ↑A.domain ∧
      (∀ (lambda : ℝ), omega < lambda → lambda ∈ A.resolventSet) ∧
        ∀ (lambda : ℝ), omega < lambda → ‖A.resolvent lambda‖ ≤ (lambda - omega)⁻¹

Hille--Yosida generation theorem. Formalized in Tau Ceti as TauCeti.Semigroups.hilleYosida_generation.

TauCeti.Semigroups.hilleYosida_generation.{u_1} {X : Type u_1} [NormedAddCommGroup X]
  [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {M omega : ℝ} (hM : 1 ≤ M)
  (hres : ∀ (lambda : ℝ), omega < lambda → lambda ∈ A.resolventSet)
  (hpow :
    ∀ (n : ℕ),
      1 ≤ n → ∀ (lambda : ℝ), omega < lambda → ‖A.resolvent lambda ^ n‖ ≤ M / (lambda - omega) ^ n)
  (hdense : Dense ↑A.domain) : ∃ S, S.generator = A ∧ S.HasGrowthBound omega M
Sources
LeanTauCeti.Semigroups.exists_contractionSemigroup_generator_eq_iff_forall_norm_resolvent_le · TauCeti.Semigroups.exists_generator_eq_and_hasGrowthBound_one_iff_forall_norm_resolvent_le · TauCeti.Semigroups.hilleYosida_generation
Uses 3
Proof usesThe Duhamel identity for the exponential of a bounded operator · Hille--Yosida characterization · Lumer--Phillips in duality-map form

TheoremStone's theorem#

An operator A on a complex Hilbert space is self-adjoint if and only if i • A is the complex generator of a unitary C₀-group.

LinearPMap.isSelfAdjoint_iff_exists_isUnitary_complexGenerator_eq_I_smul.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (A : H →ₗ.[ℂ] H) :
  IsSelfAdjoint A ↔ ∃ U, ∃ (hU : U.IsUnitary), U.complexGenerator hU = Complex.I • A
Lean

Formalized in Tau Ceti as LinearPMap.isSelfAdjoint_iff_exists_isUnitary_complexGenerator_eq_I_smul.

Other forms

Stone's theorem, converse direction. Formalized in Tau Ceti as IsSelfAdjoint.existsUnique_isUnitary_complexGenerator_eq_I_smul.

IsSelfAdjoint.existsUnique_isUnitary_complexGenerator_eq_I_smul.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →ₗ.[ℂ] H}
  (hA : IsSelfAdjoint A) : ∃! U, ∃ (hU : U.IsUnitary), U.complexGenerator hU = Complex.I • A

Stone's theorem, converse direction (existence). Formalized in Tau Ceti as IsSelfAdjoint.exists_isUnitary_complexGenerator_eq_I_smul.

IsSelfAdjoint.exists_isUnitary_complexGenerator_eq_I_smul.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →ₗ.[ℂ] H}
  (hA : IsSelfAdjoint A) : ∃ U, ∃ (hU : U.IsUnitary), U.complexGenerator hU = Complex.I • A
Sources
LeanLinearPMap.isSelfAdjoint_iff_exists_isUnitary_complexGenerator_eq_I_smul · IsSelfAdjoint.existsUnique_isUnitary_complexGenerator_eq_I_smul · IsSelfAdjoint.exists_isUnitary_complexGenerator_eq_I_smul
Uses 1
Proof usesLumer--Phillips in duality-map form

TheoremHausdorff--Bernstein--Widder theorem, finite-measure version on ℝ≥0#

A function is continuous on [0, ∞) and completely monotone on (0, ∞) if and only if it is the Laplace transform of a finite positive measure on ℝ≥0.

TauCeti.hausdorff_bernstein_widder (f : ℝ → ℝ) :
  TauCeti.IsContinuousCompletelyMonotoneOnIoi f ↔ ∃ μ, TauCeti.RepresentsLaplace μ f
Lean

Formalized in Tau Ceti as TauCeti.hausdorff_bernstein_widder.

Other forms

The Hausdorff--Bernstein--Widder theorem in finite-difference form. Formalized in Tau Ceti as TauCeti.hausdorff_bernstein_widder_difference.

TauCeti.hausdorff_bernstein_widder_difference (f : ℝ → ℝ) :
  TauCeti.IsDifferenceCompletelyMonotone f ∧ ContinuousWithinAt f (Set.Ici 0) 0 ↔
    ∃ μ, TauCeti.RepresentsLaplace μ f

The Hausdorff--Bernstein--Widder theorem on the open half-line. Formalized in Tau Ceti as TauCeti.hausdorff_bernstein_widder_onIoi.

TauCeti.hausdorff_bernstein_widder_onIoi (f : ℝ → ℝ) :
  TauCeti.IsCompletelyMonotoneOnIoi f ↔ ∃ μ, TauCeti.RepresentsLaplaceOnIoi μ f
Sources
LeanTauCeti.hausdorff_bernstein_widder · TauCeti.hausdorff_bernstein_widder_difference · TauCeti.hausdorff_bernstein_widder_onIoi
Uses 3 · Used by 2
Proof usesBernstein's theorem, existence half · Existence half of the Hausdorff--Bernstein--Widder theorem · Moment determinacy, exponential-moment form (the roadmap's B1 hypothesis)
Used byThe Berg--Christensen--Ressel representation theorem (Berg--Christensen--Ressel 4.1.13) · The zero-spatial BCR theorem is the Hausdorff--Bernstein--Widder theorem

TheoremBochner's characterization without countability assumptions#

A function on a locally compact abelian group is continuous and positive definite if and only if it is the Fourier–Stieltjes transform of a unique finite inner regular measure on the Pontryagin dual.

TauCeti.continuous_and_isPositiveDefiniteSub_iff_existsUnique_innerRegular_pontryaginMeasureTransform_eq.{u_1}
  {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G]
  [LocallyCompactSpace G] [MeasurableSpace (PontryaginDual (Multiplicative G))]
  [BorelSpace (PontryaginDual (Multiplicative G))] (φ : G → ℂ) :
  Continuous φ ∧ TauCeti.IsPositiveDefiniteSub φ ↔
    ∃! μ, (↑μ).InnerRegular ∧ μ.pontryaginMeasureTransform = φ
Lean

Formalized in Tau Ceti as TauCeti.continuous_and_isPositiveDefiniteSub_iff_existsUnique_innerRegular_pontryaginMeasureTransform_eq.

Sources
LeanTauCeti.continuous_and_isPositiveDefiniteSub_iff_existsUnique_innerRegular_pontryaginMeasureTransform_eq
Uses 1
Proof usesBochner's theorem

TheoremBochner's theorem#

A function F on a finite-dimensional real inner-product space is continuous and positive definite if and only if it is the Fourier-convention transform v ↦ ∫ q, fourierAtom v q ∂μ of a unique finite Borel measure μ. Bochner (1932); Rudin, Fourier Analysis on Groups, Theorem 1.4.3.

TauCeti.bochner.{u_1} {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (F : V → ℂ) :
  Continuous F ∧ TauCeti.IsPositiveDefiniteSub F ↔
    ∃! μ, MeasureTheory.IsFiniteMeasure μ ∧ ∀ (v : V), F v = ∫ (q : V), TauCeti.fourierAtom v q ∂μ
Lean

Formalized in Tau Ceti as TauCeti.bochner.

Other forms

Bochner's theorem for normalized functions. Formalized in Tau Ceti as TauCeti.bochner_probabilityMeasure.

TauCeti.bochner_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 μ ∧ ∀ (v : V), F v = ∫ (q : V), TauCeti.fourierAtom v q ∂μ

Bochner's theorem on ℝᵈ. Formalized in Tau Ceti as TauCeti.bochner_euclideanSpace.

TauCeti.bochner_euclideanSpace (d : ℕ) (F : EuclideanSpace ℝ (Fin d) → ℂ) :
  Continuous F ∧ TauCeti.IsPositiveDefiniteSub F ↔
    ∃! μ,
      MeasureTheory.IsFiniteMeasure μ ∧
        ∀ (v : EuclideanSpace ℝ (Fin d)),
          F v = ∫ (q : EuclideanSpace ℝ (Fin d)), TauCeti.fourierAtom v q ∂μ

Bochner's theorem on a discrete abelian group. Formalized in Tau Ceti as TauCeti.isPositiveDefiniteSub_iff_exists_pontryaginMeasureTransform_eq.

TauCeti.isPositiveDefiniteSub_iff_exists_pontryaginMeasureTransform_eq.{u_1} {G : Type u_1}
  [AddCommGroup G] [TopologicalSpace G] [DiscreteTopology G]
  [MeasurableSpace (PontryaginDual (Multiplicative G))]
  [BorelSpace (PontryaginDual (Multiplicative G))] (φ : G → ℂ) :
  TauCeti.IsPositiveDefiniteSub φ ↔ ∃ μ, (↑μ).InnerRegular ∧ μ.pontryaginMeasureTransform = φ

Bochner's theorem on a locally compact abelian group, existence half. Formalized in Tau Ceti as TauCeti.IsPositiveDefiniteSub.exists_pontryaginMeasureTransform_eq_of_continuousAt.

TauCeti.IsPositiveDefiniteSub.exists_pontryaginMeasureTransform_eq_of_continuousAt.{u_1}
  {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G]
  [LocallyCompactSpace G] [MeasurableSpace (PontryaginDual (Multiplicative G))]
  [BorelSpace (PontryaginDual (Multiplicative G))] {φ : G → ℂ}
  (hφ : TauCeti.IsPositiveDefiniteSub φ) (hφ₀ : ContinuousAt φ 0) :
  ∃ μ, (↑μ).InnerRegular ∧ μ.pontryaginMeasureTransform = φ

Bochner's theorem on the real line, in its classical form. Formalized in Tau Ceti as TauCeti.bochner_charFun_real.

TauCeti.bochner_charFun_real (F : ℝ → ℂ) :
  Continuous F ∧ TauCeti.IsPositiveDefiniteSub F ↔
    ∃! μ,
      MeasureTheory.IsFiniteMeasure μ ∧
        ∀ (x : ℝ), F x = ∫ (ξ : ℝ), Complex.exp (↑x * ↑ξ * Complex.I) ∂μ

Bochner's theorem, characteristic-function form. Formalized in Tau Ceti as TauCeti.bochner_charFun.

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

Bochner's theorem, kernel form. Formalized in Tau Ceti as TauCeti.bochner_posSemidef.

TauCeti.bochner_posSemidef.{u_1} {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (F : V → ℂ) :
  (Continuous F ∧ Matrix.PosSemidef fun a b => F (a - b)) ↔
    ∃! μ, MeasureTheory.IsFiniteMeasure μ ∧ ∀ (v : V), F v = ∫ (q : V), TauCeti.fourierAtom v q ∂μ
Sources
LeanTauCeti.bochner · TauCeti.bochner_probabilityMeasure · TauCeti.bochner_euclideanSpace · TauCeti.isPositiveDefiniteSub_iff_exists_pontryaginMeasureTransform_eq · TauCeti.IsPositiveDefiniteSub.exists_pontryaginMeasureTransform_eq_of_continuousAt · TauCeti.bochner_charFun_real · TauCeti.bochner_charFun · TauCeti.bochner_posSemidef
Uses 6 · Used by 3
Proof usesConverse half of Bochner's theorem · Existence half of Bochner's theorem · Lévy's continuity theorem, including existence · The representing measure of Bochner's theorem · Spectral theorem for strongly continuous unitary representations, cyclic form · Uniqueness half of Bochner's theorem
Used byThe Bochner–Khinchin theorem · Bochner's characterization without countability assumptions · The Berg--Christensen--Ressel representation theorem (Berg--Christensen--Ressel 4.1.13)

TheoremThe Berg--Christensen--Ressel representation theorem (Berg--Christensen--Ressel 4.1.13)#

A function on the involutive semigroup ℝ≥0 × V, for V a finite-dimensional real inner-product space, is positive definite, continuous and bounded if and only if it is the Laplace--Fourier transform of a unique finite measure on ℝ≥0 × V:

F (t, a) = ∫ (p, q), exp (-t p) * exp (-2πi⟪a, q⟫) dμ (p, q).

The forward direction is TauCeti.exists_representsLaplaceFourier together with the transform injectivity of TauCeti.RepresentsLaplaceFourier.unique; the converse direction is the elementary fact that such a transform is positive definite, continuous, and bounded by the total mass.

TauCeti.bcr_semigroup_bochner.{u_1} {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (F : NNReal × V → ℂ) :
  TauCeti.IsSemigroupGroupPD F ∧ Continuous F ∧ Bornology.IsBounded (Set.range F) ↔
    ∃! μ, TauCeti.RepresentsLaplaceFourier μ F
Lean

Formalized in Tau Ceti as TauCeti.bcr_semigroup_bochner.

Sources
LeanTauCeti.bcr_semigroup_bochner
Uses 7 · Used by 1
Proof usesBochner's theorem · Converse half of Bochner's theorem · Existence half of the Hausdorff--Bernstein--Widder theorem · Hausdorff--Bernstein--Widder theorem, finite-measure version on ℝ≥0 · Moment determinacy, exponential-moment form (the roadmap's B1 hypothesis) · The representing measure of Bochner's theorem · Uniqueness half of Bochner's theorem
Used byThe zero-spatial BCR theorem is the Hausdorff--Bernstein--Widder theorem

TheoremTauCeti.Semigroups.StronglyContinuousSemigroup.ofBounded_resolvent_eq_inv_smul_tsum_pow#

For λ > ‖A‖, the Laplace-transform resolvent of t ↦ exp (tA) is the Neumann series λ⁻¹ ∑' n, (λ⁻¹ A)ⁿ.

TauCeti.Semigroups.StronglyContinuousSemigroup.ofBounded_resolvent_eq_inv_smul_tsum_pow.{u_1}
  {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →L[ℝ] X)
  {lambda : ℝ} (hlambda : ‖A‖ < lambda) :
  (TauCeti.Semigroups.StronglyContinuousSemigroup.ofBounded A).resolvent ⋯ lambda hlambda =
    lambda⁻¹ • ∑' (n : ℕ), (lambda⁻¹ • A) ^ n
Lean

Formalized in Tau Ceti as TauCeti.Semigroups.StronglyContinuousSemigroup.ofBounded_resolvent_eq_inv_smul_tsum_pow.

Sources
LeanTauCeti.Semigroups.StronglyContinuousSemigroup.ofBounded_resolvent_eq_inv_smul_tsum_pow

StructureTauCeti.Complexification#

The complexification X ⊕ i X of a real vector space X: an element with real part re and imaginary part im stands for the formal sum re + i im.

TauCeti.Complexification.{u_1} (X : Type u_1) : Type u_1
Lean

Formalized in Tau Ceti as TauCeti.Complexification.

Sources
LeanTauCeti.Complexification
Used by 1
Used byPolar decomposition of a bounded operator

TheoremThe Laplace transform turns convolution into multiplication#

The identity needs no finiteness or integrability hypothesis: under the junk-value convention for non-integrable Bochner integrals it holds for all s-finite measures and every real parameter t.

TauCeti.laplaceTransform_conv (μ ν : MeasureTheory.Measure NNReal) [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν] (t : ℝ) :
  TauCeti.laplaceTransform (μ.conv ν) t =
    TauCeti.laplaceTransform μ t * TauCeti.laplaceTransform ν t
Lean

Formalized in Tau Ceti as TauCeti.laplaceTransform_conv.

Sources
LeanTauCeti.laplaceTransform_conv

TheoremConverse half of Bochner's theorem#

The Fourier-convention transform of a finite Borel measure is continuous and positive definite.

TauCeti.continuous_and_isPositiveDefiniteSub_of_integral_fourierAtom_eq.{u_1} {V : Type u_1}
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V]
  [BorelSpace V] {F : V → ℂ} (μ : MeasureTheory.Measure V) [MeasureTheory.IsFiniteMeasure μ]
  (hrep : ∀ (v : V), F v = ∫ (q : V), TauCeti.fourierAtom v q ∂μ) :
  Continuous F ∧ TauCeti.IsPositiveDefiniteSub F
Lean

Formalized in Tau Ceti as TauCeti.continuous_and_isPositiveDefiniteSub_of_integral_fourierAtom_eq.

Sources
LeanTauCeti.continuous_and_isPositiveDefiniteSub_of_integral_fourierAtom_eq
Used by 2
Used byBochner's theorem · The Berg--Christensen--Ressel representation theorem (Berg--Christensen--Ressel 4.1.13)

TheoremExistence half of Bochner's theorem#

A continuous positive-definite function F on a finite-dimensional real inner-product space is the Fourier-convention transform v ↦ ∫ q, fourierAtom v q ∂μ of a finite Borel measure μ. Rudin, Fourier Analysis on Groups, Theorem 1.4.3.

TauCeti.exists_isFiniteMeasure_integral_fourierAtom_eq.{u_1} {V : Type u_1} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (F : V → ℂ)
  (hcont : Continuous F) (hpd : TauCeti.IsPositiveDefiniteSub F) :
  ∃ μ, MeasureTheory.IsFiniteMeasure μ ∧ ∀ (v : V), F v = ∫ (q : V), TauCeti.fourierAtom v q ∂μ
Lean

Formalized in Tau Ceti as TauCeti.exists_isFiniteMeasure_integral_fourierAtom_eq.

Sources
LeanTauCeti.exists_isFiniteMeasure_integral_fourierAtom_eq
Uses 1 · Used by 1
Proof usesLévy's continuity theorem, including existence
Used byBochner's theorem

TheoremExistence half of the Hausdorff--Bernstein--Widder theorem#

a function continuous on [0, ∞) and completely monotone on (0, ∞) is the Laplace transform of a finite positive measure on ℝ≥0.

TauCeti.exists_representsLaplace_of_isContinuousCompletelyMonotoneOnIoi {f : ℝ → ℝ}
  (hf : TauCeti.IsContinuousCompletelyMonotoneOnIoi f) : ∃ μ, TauCeti.RepresentsLaplace μ f
Lean

Formalized in Tau Ceti as TauCeti.exists_representsLaplace_of_isContinuousCompletelyMonotoneOnIoi.

Other forms

The existence half of the Hausdorff--Bernstein--Widder theorem in finite-difference form. Formalized in Tau Ceti as TauCeti.exists_representsLaplace_of_isDifferenceCompletelyMonotone_of_continuousWithinAt.

TauCeti.exists_representsLaplace_of_isDifferenceCompletelyMonotone_of_continuousWithinAt {f : ℝ → ℝ}
  (hf : TauCeti.IsDifferenceCompletelyMonotone f) (hcont : ContinuousWithinAt f (Set.Ici 0) 0) :
  ∃ μ, TauCeti.RepresentsLaplace μ f
Sources
LeanTauCeti.exists_representsLaplace_of_isContinuousCompletelyMonotoneOnIoi · TauCeti.exists_representsLaplace_of_isDifferenceCompletelyMonotone_of_continuousWithinAt
Uses 2 · Used by 2
Proof usesBernstein's theorem, existence half · Prokhorov's theorem for finite measures
Used byHausdorff--Bernstein--Widder theorem, finite-measure version on ℝ≥0 · The Berg--Christensen--Ressel representation theorem (Berg--Christensen--Ressel 4.1.13)

DefinitionThe representing measure of Bochner's theorem#

the unique finite Borel measure whose Fourier-convention transform is F, when F is continuous and positive definite, and the zero measure otherwise.

TauCeti.bochnerMeasure.{u_1} {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (F : V → ℂ) : MeasureTheory.Measure V
Informally uses
Lean

Formalized in Tau Ceti as TauCeti.bochnerMeasure.

Sources
LeanTauCeti.bochnerMeasure
Used by 2
Used byBochner'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.