ProjectionFieldReduction.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

Reducing operator fields to their projection fibers

Each orthogonal projection has an actual closed Hilbert range. Compression of a supported operator to this range preserves its norm and action. These constructions are pointwise, so they apply to every fixed operator field; no simultaneous representation law on an uncountable algebra is required.

def OAI.KadisonSimilarity.projectionFiber line 21
Source documentation
The actual closed range of an orthogonal projection.
```
def projectionFiber (p : H →L[ℂ] H) (hp : IsStarProjection p) : ClosedSubmodule ℂ H :=
…
```
def OAI.KadisonSimilarity.projectionFiberInclusion line 24
def OAI.KadisonSimilarity.projectionFiberRetraction line 27
theorem OAI.KadisonSimilarity.projectionFiberRetraction_coe line 30
theorem OAI.KadisonSimilarity.projectionFiber_fixed line 33
theorem OAI.KadisonSimilarity.projectionFiberRetraction_inclusion line 40
theorem OAI.KadisonSimilarity.norm_projectionFiberRetraction_le line 48
def OAI.KadisonSimilarity.projectionFiberCompression line 57
Source documentation
Compression is defined on every operator, even before support is proved.
```
def projectionFiberCompression (p : H →L[ℂ] H) (hp : IsStarProjection p) (T : H →L[ℂ] H) :
    projectionFiber p hp →L[ℂ] projectionFiber p hp :=
…
```
Mentions: OAI.KadisonSimilarity.projectionFiber
theorem OAI.KadisonSimilarity.projectionFiberCompression_coe line 61
theorem OAI.KadisonSimilarity.projectionFiberCompression_apply_of_left_support line 66
Source documentation
A left-supported operator retains its actual action on the range.
```
theorem projectionFiberCompression_apply_of_left_support
    (p : H →L[ℂ] H) (hp : IsStarProjection p) (T : H →L[ℂ] H) (hT : p * T = T)
    (x : projectionFiber p hp) : (projectionFiberCompression p hp T x : H) = T x :=
…
```
Mentions: OAI.KadisonSimilarity.projectionFiber, OAI.KadisonSimilarity.projectionFiberCompression

theorem OAI.KadisonSimilarity.projectionFiberCompression_extension line 72

Source documentation

Extending the compressed supported operator by zero recovers it.

theorem projectionFiberCompression_extension
    (p : H →L[ℂ] H) (hp : IsStarProjection p) (T : H →L[ℂ] H)
    (hleft : p * T = T) (hright : T * p = T) :
    (projectionFiberInclusion p hp).toContinuousLinearMap.comp
      ((projectionFiberCompression p hp T).comp (projectionFiberRetraction p hp)) = T := by
…

Mentions: OAI.KadisonSimilarity.projectionFiberInclusion, OAI.KadisonSimilarity.projectionFiberCompression, OAI.KadisonSimilarity.projectionFiberRetraction

theorem OAI.KadisonSimilarity.norm_projectionFiberCompression line 85

Source documentation

No norm is lost by restricting a supported operator to the projection range.

theorem norm_projectionFiberCompression
    (p : H →L[ℂ] H) (hp : IsStarProjection p) (T : H →L[ℂ] H)
    (hleft : p * T = T) (hright : T * p = T) :
    ‖projectionFiberCompression p hp T‖ = ‖T‖ := by
…

Mentions: OAI.KadisonSimilarity.projectionFiberCompression

theorem OAI.KadisonSimilarity.norm_matrix_projectionFiberCompression line 99

Source documentation

The same supported restriction preserves every finite operator-matrix norm; the coordinate inclusions and retractions remain contractive.

theorem norm_matrix_projectionFiberCompression
    (p : H →L[ℂ] H) (hp : IsStarProjection p) {n : ℕ}
    (X : Matrix (Fin n) (Fin n) (H →L[ℂ] H))
    (hleft : ∀ i j, p * X i j = X i j) (hright : ∀ i j, X i j * p = X i j) :
    ‖matrixOperator (fun i j => projectionFiberCompression p hp (X i j))‖ =
      ‖matrixOperator X‖ := by
…

Mentions: OAI.KadisonSimilarity.matrixOperator, OAI.KadisonSimilarity.projectionFiberCompression

theorem OAI.KadisonSimilarity.projectionFiber_invariant line 139
def OAI.KadisonSimilarity.projectionFiberAction line 147
Source documentation
A commuting operator acts on the closed range by ordinary restriction.
```
def projectionFiberAction (p : H →L[ℂ] H) (hp : IsStarProjection p)
    (T : H →L[ℂ] H) (hcomm : Commute p T) :
    projectionFiber p hp →L[ℂ] projectionFiber p hp :=
…
```
Mentions: OAI.KadisonSimilarity.projectionFiber
theorem OAI.KadisonSimilarity.projectionFiberAction_coe line 152
theorem OAI.KadisonSimilarity.projectionFiberAction_eq_compression line 156
def OAI.KadisonSimilarity.projectionFiberRepresentation line 168
Source documentation
A genuine representation commuting with a projection restricts to a genuine unital representation on its actual Hilbert range.
```
def projectionFiberRepresentation (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (p : H →L[ℂ] H) (hp : IsStarProjection p) (hcomm : ∀ a, Commute p (σ a)) :
    A →⋆ₐ[ℂ] (projectionFiber p hp →L[ℂ] projectionFiber p hp) where
…
```
Mentions: OAI.KadisonSimilarity.projectionFiber
theorem OAI.KadisonSimilarity.projectionFiberRepresentation_coe line 190

theorem OAI.KadisonSimilarity.ae_field_left_support line 205

Source documentation

An actual left-support identity gives the corresponding field identity almost everywhere.

theorem ae_field_left_support
    (P T : Lp H 2 μ →L[ℂ] Lp H 2 μ) (p R : Ω → H →L[ℂ] H)
    (hP : ∀ f : Lp H 2 μ, ∀ᵐ a ∂μ, P f a = p a (f a))
    (hR : ∀ f : Lp H 2 μ, ∀ᵐ a ∂μ, T f a = R a (f a))
    (hPT : P * T = T) : ∀ᵐ a ∂μ, p a * R a = R a := by
…

theorem OAI.KadisonSimilarity.ae_field_right_support line 215

Source documentation

Right support is also inherited from the actual L² operator equation.

theorem ae_field_right_support
    (P T : Lp H 2 μ →L[ℂ] Lp H 2 μ) (p R : Ω → H →L[ℂ] H)
    (hP : ∀ f : Lp H 2 μ, ∀ᵐ a ∂μ, P f a = p a (f a))
    (hR : ∀ f : Lp H 2 μ, ∀ᵐ a ∂μ, T f a = R a (f a))
    (hTP : T * P = T) : ∀ᵐ a ∂μ, R a * p a = R a := by
…

theorem OAI.KadisonSimilarity.ae_norm_projectionFiberCompression line 225

Source documentation

Restricting supported fields to their projection fibers loses no pointwise norm, with support derived from the original operators.

theorem ae_norm_projectionFiberCompression
    (P T : Lp H 2 μ →L[ℂ] Lp H 2 μ) (p R : Ω → H →L[ℂ] H)
    (hp : ∀ a, IsStarProjection (p a))
    (hP : ∀ f : Lp H 2 μ, ∀ᵐ a ∂μ, P f a = p a (f a))
    (hR : ∀ f : Lp H 2 μ, ∀ᵐ a ∂μ, T f a = R a (f a))
    (hPT : P * T = T) (hTP : T * P = T) :
    ∀ᵐ a ∂μ, ‖projectionFiberCompression (p a) (hp a) (R a)‖ = ‖R a‖ := by
…

Mentions: OAI.KadisonSimilarity.projectionFiberCompression

theorem OAI.KadisonSimilarity.projectionFiberCompression_section_action line 238

Source documentation

The restricted field has the same action on every section taking values in the projection fibers.

theorem projectionFiberCompression_section_action
    (P T : Lp H 2 μ →L[ℂ] Lp H 2 μ) (p R : Ω → H →L[ℂ] H)
    (hp : ∀ a, IsStarProjection (p a))
    (hP : ∀ f : Lp H 2 μ, ∀ᵐ a ∂μ, P f a = p a (f a))
    (hR : ∀ f : Lp H 2 μ, ∀ᵐ a ∂μ, T f a = R a (f a))
    (hPT : P * T = T) (f : Lp H 2 μ)
    (v : ∀ a, projectionFiber (p a) (hp a))
    (hv : ∀ᵐ a ∂μ, (v a : H) = f a) :
    ∀ᵐ a ∂μ, (projectionFiberCompression (p a) (hp a) (R a) (v a) : H) = T f a := by
…

Mentions: OAI.KadisonSimilarity.projectionFiber, OAI.KadisonSimilarity.projectionFiberCompression