ParameterOpenness.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Filling an open neighborhood with physical parameters

The finite-dimensional step used in the proof of Theorem thm:blowup. Brouwer's theorem gives a zero for a continuous perturbation of an invertible linear parameter map when the boundary error is sufficiently small.

theorem OAI.DefocusingNLS.continuous_perturbation_covers_ball line 18

Source documentation

A continuous perturbation of the identity on a ball covers the smaller ball.

theorem continuous_perturbation_covers_ball {E : Type*}
    [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    (r δ : ℝ) (hr : 0 ≤ r)
    (f : closedBall (0 : E) r → E) (hf : Continuous f)
    (herror : ∀ x, ‖f x - x.val‖ ≤ δ) :
    closedBall (0 : E) (r - δ) ⊆ Set.range f := by
…

theorem OAI.DefocusingNLS.zero_of_small_continuous_error line 46

Source documentation

The zero-existence specialization used after preconditioning by the invertible physical-parameter matrix.

theorem zero_of_small_continuous_error {E : Type*}
    [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    (r δ : ℝ) (hr : 0 ≤ r) (hδ : δ ≤ r)
    (f : closedBall (0 : E) r → E) (hf : Continuous f)
    (herror : ∀ x, ‖f x - x.val‖ ≤ δ) :
    ∃ x, f x = 0 := by
…

theorem OAI.DefocusingNLS.zero_of_near_invertible_linear_map line 57

Source documentation

The version applied to a map close to an invertible physical-parameter matrix, after multiplication by its inverse.

theorem zero_of_near_invertible_linear_map {E : Type*}
    [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    (C : E ≃L[ℝ] E) (r δ : ℝ) (hr : 0 ≤ r) (hδ : δ ≤ r)
    (f : closedBall (0 : E) r → E) (hf : Continuous f)
    (herror : ∀ x, ‖C.symm (f x) - x.val‖ ≤ δ) :
    ∃ x, f x = 0 := by
…

abbrev OAI.DefocusingNLS.PhysicalParameters line 69
Source documentation
Phase, twelve translations, and logarithmic blowup time.
```
abbrev PhysicalParameters := ℝ × (Fin 12 → ℝ) × ℝ
```
def OAI.DefocusingNLS.leadingParameterMap line 72
Source documentation
The leading parameter map in equation nl:leading-expansion.
```
def leadingParameterMap (b : ℝ) (d : PhysicalParameters) : PhysicalParameters :=
…
```
Mentions: OAI.DefocusingNLS.PhysicalParameters
theorem OAI.DefocusingNLS.leadingParameterMap_involutive line 76
Source documentation
The leading matrix is its own inverse, for every phase frequency.
```
theorem leadingParameterMap_involutive (b : ℝ) :
    Function.Involutive (leadingParameterMap b) := by
…
```
Mentions: OAI.DefocusingNLS.leadingParameterMap