GaussianSupport.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Supporting probability lemmas for stable defocusing NLS blowup

These lemmas formalize the measure and quantifier steps in the proof of Corollary 1.2 of Stable self-similar blowup for a supercritical defocusing Schrödinger equation on the torus (September 2026). The independent head/tail argument uses Mathlib's measure-theoretic independence theorem.

theorem OAI.DefocusingNLS.positive_sublevel_of_lintegral_lt line 27
Source documentation
If the expectation of a nonnegative random variable is below a threshold, its strict sublevel set has positive probability. Applied to the squared tail norm, this supplies the tail event in the Fourier support argument.
```
theorem positive_sublevel_of_lintegral_lt {Ω : Type*} [MeasurableSpace Ω]
    {μ : Measure Ω} [IsProbabilityMeasure μ] {F : Ω → ℝ≥0∞} {c : ℝ≥0∞}
    (hmean : (∫⁻ ω, F ω ∂μ) < c) : 0 < μ {ω | F ω < c} := by
…
```

theorem OAI.DefocusingNLS.positive_ball_of_independent_head_tail line 48

Source documentation

Independent positive-probability head and tail events put the full random variable in a prescribed ball with positive probability.

theorem positive_ball_of_independent_head_tail
    (happrox : ‖f - g‖ < r / 3)
    (hhead : 0 < μ {ω | ‖H ω - g‖ < r / 3})
    (htail : 0 < μ {ω | ‖X ω - H ω‖ < r / 3})
    (hindep : IndepSet {ω | ‖H ω - g‖ < r / 3}
      {ω | ‖X ω - H ω‖ < r / 3} μ) :
    0 < μ (X ⁻¹' Metric.ball f r) := by
…

theorem OAI.DefocusingNLS.positive_open_of_head_tail line 76

Source documentation

Nonempty open sets have positive probability whenever the above head/tail approximation can be made at every center and radius. This is the exact measure-theoretic part of the Gaussian support argument.

theorem positive_open_of_head_tail
    (hsplit : ∀ (f : E) (r : ℝ), 0 < r →
      ∃ (H : Ω → E) (g : E), ‖f - g‖ < r / 3 ∧
        0 < μ {ω | ‖H ω - g‖ < r / 3} ∧
        0 < μ {ω | ‖X ω - H ω‖ < r / 3} ∧
        IndepSet {ω | ‖H ω - g‖ < r / 3}
          {ω | ‖X ω - H ω‖ < r / 3} μ)
    {U : Set E} (hU : IsOpen U) (hne : U.Nonempty) :
    0 < μ (X ⁻¹' U) := by
…

theorem OAI.DefocusingNLS.not_ae_of_positive_bad_set line 96
Source documentation
A positive-probability set of data incompatible with global continuation rules out almost-sure global continuation. No measurability of the bad-data predicate is needed for this implication.
```
theorem not_ae_of_positive_bad_set {B : Set E} {Good : E → Prop}
    (hB : 0 < μ (X ⁻¹' B)) (hbad : ∀ x ∈ B, ¬ Good x) :
    ¬ ∀ᵐ ω ∂μ, Good (X ω) := by
…
```

theorem OAI.DefocusingNLS.no_universal_regularity_threshold line 111

Source documentation

The fixed index supplied by the deterministic theorem refutes every finite Gaussian regularity threshold, with the strict inequalities in the manuscript.

theorem no_universal_regularity_threshold {Global : ℝ → ℝ → Prop} {k : ℝ}
    (hk : 8 < k) (hfailure : ∀ α : ℝ, k + 6 < α → ¬ Global α k) :
    ¬ ∃ α₀ : ℝ, ∀ α : ℝ, α₀ < α →
      ∀ m : ℝ, 8 < m → m < α - 6 → Global α m := by
…