ExpandingDuhamelContinuity.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Continuity of the moving-scale Duhamel map

Rescaling the integration time to the fixed unit interval gives strong continuity, including at time zero, without operator-norm continuity.

def OAI.DefocusingNLS.unitTime line 19
def OAI.DefocusingNLS.expandingDuhamelParameters line 22
theorem OAI.DefocusingNLS.continuous_expandingDuhamelParameters line 29
def OAI.DefocusingNLS.expandingUnitDuhamelIntegrand line 43
theorem OAI.DefocusingNLS.continuous_expandingUnitDuhamelIntegrand line 49
theorem OAI.DefocusingNLS.expandingUnitDuhamelIntegrand_eq line 62
theorem OAI.DefocusingNLS.expandingDuhamel_eq_unitIntegral line 75
Source documentation
A fixed unit-interval integral represents the moving-scale Duhamel term exactly.
```
theorem expandingDuhamel_eq_unitIntegral (a b k : ℝ)
    (ha : 0 < a) (hk : 8 < k) (r : ℝ → FourierL2)
    (p : ExpandingFreeParameters) :
    expandingDuhamel a b k p.1.1 ha hk p.1.2 p.2 r =
      (p.2 : ℝ) • ∫ u in Icc (0 : ℝ) 1,
        expandingUnitDuhamelIntegrand a b k ha hk r p u := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.ExpandingFreeParameters, OAI.DefocusingNLS.expandingDuhamel, OAI.DefocusingNLS.expandingUnitDuhamelIntegrand
theorem OAI.DefocusingNLS.continuous_expandingDuhamel line 95
Source documentation
The inhomogeneous solution depends strongly continuously on starting scale and time.
```
theorem continuous_expandingDuhamel (a b k : ℝ)
    (ha : 0 < a) (hk : 8 < k) (r : ℝ → FourierL2) (hr : Continuous r) :
    Continuous (fun p : ExpandingFreeParameters =>
      expandingDuhamel a b k p.1.1 ha hk p.1.2 p.2 r) := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.ExpandingFreeParameters, OAI.DefocusingNLS.expandingDuhamel

theorem OAI.DefocusingNLS.continuousOn_expandingDuhamel line 111

Source documentation

Continuous forcing on a closed time slab yields a continuous inhomogeneous solution.

theorem continuousOn_expandingDuhamel (a b k L T : ℝ)
    (ha : 0 < a) (hk : 8 < k) (hL : 1 ≤ L) (hT : 0 ≤ T)
    (r : ℝ → FourierL2) (hr : ContinuousOn r (Icc 0 T)) :
    ContinuousOn (fun t => expandingDuhamel a b k L ha hk hL t r) (Icc 0 T) := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.expandingDuhamel