HilbertProjections.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

Baire continuity points from rational sublevel boundaries, without a global boundedness assumption.

def OAI.Generator.continuityCore line 20
Source documentation
An explicit countable intersection of open sets of continuity points.
```
def continuityCore (f : X → ℝ) : Set X :=
…
```
theorem OAI.Generator.continuityCore_isGδ line 23
theorem OAI.Generator.continuityCore_dense line 26
theorem OAI.Generator.continuousAt_of_mem_continuityCore line 32

theorem OAI.Generator.common_continuity_core line 47

Source documentation

The common continuity set for a countable family, as used before extending the projection-norm conclusion to all L2 vectors.

theorem common_continuity_core [BaireSpace X] (f : ℕ → X → ℝ)
    (hf : ∀ n, LowerSemicontinuous (f n)) :
    ∃ C : Set X, IsGδ C ∧ Dense C ∧ ∀ x ∈ C, ∀ n, ContinuousAt (f n) x := by
…

theorem OAI.Generator.continuousAt_of_dense_lipschitz line 58

Source documentation

The uniform Lipschitz estimate in the vector variable extends continuity from a dense sequence to every vector (eq:projection-vector-lipschitz).

theorem continuousAt_of_dense_lipschitz {E : Type*} [PseudoMetricSpace E]
    (F : E → X → ℝ) (e : ℕ → E) (he : DenseRange e)
    (hLip : ∀ x a b, dist (F a x) (F b x) ≤ dist a b)
    {x : X} (hcont : ∀ n, ContinuousAt (F (e n)) x) (a : E) :
    ContinuousAt (F a) x := by
…

theorem OAI.Generator.common_continuity_of_lipschitz line 80

Source documentation

Baire continuity of a family of Hilbert-space projections.

theorem common_continuity_of_lipschitz [BaireSpace X]
    {E : Type*} [PseudoMetricSpace E] [TopologicalSpace.SeparableSpace E] [Nonempty E]
    (F : E → X → ℝ) (hf : ∀ a, LowerSemicontinuous (F a))
    (hLip : ∀ x a b, dist (F a x) (F b x) ≤ dist a b) :
    ∃ C : Set X, IsGδ C ∧ Dense C ∧ ∀ x ∈ C, ∀ a, ContinuousAt (F a) x := by
…

def OAI.Generator.projectionNorm line 97
theorem OAI.Generator.projectionNorm_bounds line 99
theorem OAI.Generator.projectionNorm_lipschitz line 103
theorem OAI.Generator.correlation_le_projectionNorm line 114
def OAI.Generator.residual line 122
theorem OAI.Generator.residual_projection_zero line 124
theorem OAI.Generator.residual_norm_pos line 128
theorem OAI.Generator.residual_correlation line 134

theorem OAI.Generator.common_projectionNorm_continuity line 148

Source documentation

Instantiation of the topological theorem with actual orthogonal projections. Lower semicontinuity remains an explicit prerequisite to prove for W*(P,u).

theorem common_projectionNorm_continuity {X : Type*} [TopologicalSpace X] [BaireSpace X]
    [TopologicalSpace.SeparableSpace E] (L : X → Submodule ℂ E)
    [∀ x, (L x).HasOrthogonalProjection]
    (hsemi : ∀ ξ, LowerSemicontinuous (fun x => projectionNorm (L x) ξ)) :
    ∃ C : Set X, IsGδ C ∧ Dense C ∧
      ∀ x ∈ C, ∀ ξ, ContinuousAt (fun y => projectionNorm (L y) ξ) x :=
…

Mentions: OAI.Generator.projectionNorm

def OAI.Generator.normalizedCorrelation line 163
theorem OAI.Generator.normalizedCorrelation_continuousAt line 165
theorem OAI.Generator.normalizedCorrelation_le_projectionNorm line 170
theorem OAI.Generator.normalizedCorrelation_starProjection line 183

theorem OAI.Generator.projectionNorm_lowerSemicontinuous line 198

Source documentation

Dense continuous sections imply lower semicontinuity of every projection norm. The index type need not be countable, matching the P-coefficient polynomials.

theorem projectionNorm_lowerSemicontinuous {X I : Type*} [TopologicalSpace X]
    (L : X → Submodule ℂ E) [∀ x, (L x).HasOrthogonalProjection]
    (b : I → X → E) (hb : ∀ i x, b i x ∈ L x) (hc : ∀ i, Continuous (b i))
    (hd : ∀ x, DenseRange (fun i => (⟨b i x, hb i x⟩ : L x))) (ξ : E) :
    LowerSemicontinuous (fun x => projectionNorm (L x) ξ) := by
…

Mentions: OAI.Generator.projectionNorm

theorem OAI.Generator.common_projectionNorm_continuity_of_denseSections line 234

Source documentation

The generic Hilbert-space content of lem:projection-continuity, with semicontinuity proved from dense continuous sections rather than assumed.

theorem common_projectionNorm_continuity_of_denseSections
    {X I : Type*} [TopologicalSpace X] [BaireSpace X]
    [TopologicalSpace.SeparableSpace E]
    (L : X → Submodule ℂ E) [∀ x, (L x).HasOrthogonalProjection]
    (b : I → X → E) (hb : ∀ i x, b i x ∈ L x) (hc : ∀ i, Continuous (b i))
    (hd : ∀ x, DenseRange (fun i => (⟨b i x, hb i x⟩ : L x))) :
    ∃ C : Set X, IsGδ C ∧ Dense C ∧
      ∀ x ∈ C, ∀ ξ, ContinuousAt (fun y => projectionNorm (L y) ξ) x :=
…

Mentions: OAI.Generator.projectionNorm