SobolevEmbedding.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Continuous point observation in the Fourier Sobolev model

For k > 6, the Fourier coefficients are absolutely summable in dimension twelve. Their sum is therefore a bounded linear observation (evaluation at the center of the torus), suitable for the blowup/nonextension argument.

lemma OAI.DefocusingNLS.sobolev_observation_weight_sq line 20
def OAI.DefocusingNLS.sobolevObservationVector line 29
Source documentation
The inverse Sobolev weights form an ℓ² vector exactly above dimension/2.
```
noncomputable def sobolevObservationVector (k : ℝ) (hk : 6 < k) : FourierL2 :=
…
```
Mentions: OAI.DefocusingNLS.FourierL2
def OAI.DefocusingNLS.sobolevCenterEvaluation line 36
Source documentation
Evaluation at the torus center, in the Fourier model of H^k.
```
noncomputable def sobolevCenterEvaluation (k : ℝ) (hk : 6 < k) : FourierL2 →L[ℂ] ℂ :=
…
```
Mentions: OAI.DefocusingNLS.FourierL2
theorem OAI.DefocusingNLS.hasSum_sobolevFourierCoefficient line 40
Source documentation
The bounded observation is the sum of the actual, unweighted coefficients.
```
theorem hasSum_sobolevFourierCoefficient (k : ℝ) (hk : 6 < k) (f : FourierL2) :
    HasSum (sobolevFourierCoefficient k f) (sobolevCenterEvaluation k hk f) := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.sobolevFourierCoefficient, OAI.DefocusingNLS.sobolevCenterEvaluation
theorem OAI.DefocusingNLS.sobolevCenterEvaluation_eq_tsum line 47
theorem OAI.DefocusingNLS.summable_norm_sobolevFourierCoefficient line 52
Source documentation
Absolute summability of the unweighted Fourier series.
```
theorem summable_norm_sobolevFourierCoefficient (k : ℝ) (hk : 6 < k) (f : FourierL2) :
    Summable (fun n => ‖sobolevFourierCoefficient k f n‖) :=
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.sobolevFourierCoefficient
theorem OAI.DefocusingNLS.sobolevCenterEvaluation_bound line 56

theorem OAI.DefocusingNLS.no_sobolev_extension_of_positive_center_rate line 63

Source documentation

A positive self-similar center amplitude obstructs continuous continuation in the concrete Fourier Sobolev space.

theorem no_sobolev_extension_of_positive_center_rate
    (k : ℝ) (hk : 6 < k) (u : ℝ → FourierL2) (T a c : ℝ)
    (ha : 0 < a) (hc : 0 < c)
    (hblowup : Filter.Tendsto
      (fun t => (T - t) ^ a * ‖sobolevCenterEvaluation k hk (u t)‖)
      (nhdsWithin T (Set.Iio T)) (nhds c)) :
    ¬ ContinuousWithinAt u (Set.Iio T) T :=
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.sobolevCenterEvaluation