`PhysFunctionalAnalysis.exists_atomless_sphere_measure` (E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] (e₀ e₁ : E)

Proved

PhysFunctionalAnalysis.exists_atomless_sphere_measure

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

theoremstimepiece

Prove the following Lean 4 theorem from PhysFunctionalAnalysis.

PhysFunctionalAnalysis.exists_atomless_sphere_measure (E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] (e₀ e₁ : E) (h : Orthonormal ℝ ![e₀, e₁]) : ∃ μ : Measure E, IsProbabilityMeasure μ ∧ (∀ x, μ {x} = 0) ∧ ∀ᵐ v ∂μ, ‖v‖ = 1

Formalization note: Lean 4 identifier PhysFunctionalAnalysis.exists_atomless_sphere_measure.

Preamble

-- Generated from PhysFunctionalAnalysis.lean — theorem PhysFunctionalAnalysis.exists_atomless_sphere_measure
import Mathlib
import Definitions.Def_PhysFunctionalAnalysis
import Definitions.Def_PhysMeasureBasis
import Definitions.Def_ChapterA4
open PhysMeasureBasis
open PhysFunctionalAnalysis


open MeasureTheory Set
open scoped ENNReal lp

noncomputable section


open PhysMeasureBasis

Formal statement

theorem PhysFunctionalAnalysis.exists_atomless_sphere_measure (E : Type*)
    [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
    [MeasurableSpace E] [BorelSpace E]
    (e₀ e₁ : E) (h : Orthonormal ℝ ![e₀, e₁]) :
    ∃ μ : Measure E, IsProbabilityMeasure μ ∧
      (∀ x, μ {x} = 0) ∧
      ∀ᵐ v ∂μ, ‖v‖ = 1 := by sorry

View graph