ScalarCompactExtremal.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The Hilbert-space extremal argument used for the scalar Sobolev quotient. Compactness provides a convergent image sequence; the parallelogram identity forces an extremizing sequence itself to converge.

theorem OAI.PositiveEinsteinFour.Geometry.scalar_extremizing_sequence_cauchy line 23
theorem OAI.PositiveEinsteinFour.Geometry.scalar_compact_operator_extremal line 62
Source documentation
A nonzero compact scalar Sobolev operator from a complete Hilbert space attains its norm on a unit vector.
```
theorem scalar_compact_operator_extremal [CompleteSpace H] (T : H →L[ℝ] E)
    (hcompact : IsCompactOperator T) (hT : 0 < ‖T‖) :
    ∃ u : H, ‖u‖ = 1 ∧ ‖T u‖ = ‖T‖ := by
…
```