ExpandingTransferContinuity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Operator-norm continuity of the weight identification

Only the positive weight identification is continuous in operator norm. The free Schrödinger group continues to be used with strong continuity.

theorem OAI.DefocusingNLS.expandingScaleTransfer_from_one_sub_norm_le line 17

Source documentation

A frequency-independent modulus bounds the diagonal identification operators.

theorem expandingScaleTransfer_from_one_sub_norm_le (a k L M : ℝ)
    (ha : 0 < a) (hk : 8 < k) (hL : 1 ≤ L) (hM : 1 ≤ M) :
    ‖expandingScaleTransfer a k 1 L ha hk le_rfl hL -
      expandingScaleTransfer a k 1 M ha hk le_rfl hM‖ ≤
      |L ^ a - M ^ a| + |L ^ (6 - k) - M ^ (6 - k)| := by
…

Mentions: OAI.DefocusingNLS.expandingScaleTransfer

theorem OAI.DefocusingNLS.continuous_expandingScaleTransfer_from_one line 39
Source documentation
Positive-weight identification with Y_1 is operator-norm continuous in L.
```
theorem continuous_expandingScaleTransfer_from_one (a k : ℝ) (ha : 0 < a) (hk : 8 < k) :
    Continuous (fun L : {L : ℝ // 1 ≤ L} =>
      expandingScaleTransfer a k 1 L.1 ha hk le_rfl L.2) := by
…
```
Mentions: OAI.DefocusingNLS.expandingScaleTransfer