StrongLimits.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.KervaireStrong.Operator line 13
def OAI.KervaireStrong.StrongTendsto line 15

theorem OAI.KervaireStrong.StrongTendsto.apply_variable line 20

Source documentation

Joint continuity of evaluation for strong convergence on an operator-norm bounded family.

theorem StrongTendsto.apply_variable {T : ι → Operator H} {S : Operator H}
    (h : StrongTendsto T l S) {C : ℝ} (_hC : 0 ≤ C) (hb : ∀ i, ‖T i‖ ≤ C)
    {x : ι → H} {ξ : H} (hx : Tendsto x l (𝓝 ξ)) :
    Tendsto (fun i => T i (x i)) l (𝓝 (S ξ)) := by
…

Mentions: OAI.KervaireStrong.Operator, OAI.KervaireStrong.StrongTendsto

theorem OAI.KervaireStrong.StrongTendsto.mul line 33
theorem OAI.KervaireStrong.StrongTendsto.pow line 40

theorem OAI.KervaireStrong.StrongTendsto.exp line 48

Source documentation

Exponentiation is strongly continuous on uniformly bounded families.

theorem StrongTendsto.exp [CompleteSpace H] {T : ι → Operator H} {S : Operator H}
    (h : StrongTendsto T l S) {C : ℝ} (hC : 0 ≤ C) (hb : ∀ i, ‖T i‖ ≤ C) :
    StrongTendsto (fun i => NormedSpace.exp (T i)) l (NormedSpace.exp S) := by
…

Mentions: OAI.KervaireStrong.Operator, OAI.KervaireStrong.StrongTendsto

theorem OAI.KervaireStrong.StrongTendsto.commute line 78
Source documentation
A strong limit preserves commutation with any fixed bounded operator.
```
theorem StrongTendsto.commute {T : ι → Operator H} {S R : Operator H} [l.NeBot]
    (h : StrongTendsto T l S) (hc : ∀ i, Commute (T i) R) : Commute S R := by
…
```
Mentions: OAI.KervaireStrong.Operator, OAI.KervaireStrong.StrongTendsto
theorem OAI.KervaireStrong.StrongTendsto.nonneg line 90
Source documentation
The positive cone is strongly closed, even on an uncountable Hilbert space.
```
theorem StrongTendsto.nonneg {T : ι → Operator K} {S : Operator K} [l.NeBot]
    (h : StrongTendsto T l S) (hp : ∀ i, 0 ≤ T i) : 0 ≤ S := by
…
```
Mentions: OAI.KervaireStrong.Operator, OAI.KervaireStrong.StrongTendsto