RadialGaugeLinearization.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Exact conjugation of the similarity linearization by its stationary profile.

These are pointwise identities for the actual differential expression. They supply the cancellation used in spectrum.tex, equation (spec:real-system).

def OAI.DefocusingNLS.similarityLinearization line 17
theorem OAI.DefocusingNLS.similarityLinearization_gauge line 22

theorem OAI.DefocusingNLS.similarityLinearization_logGauge line 46

Source documentation

Division of the gradient by the nonvanishing profile is the only coefficient introduced by the gauge.

theorem similarityLinearization_logGauge (a b : ℝ) (m : ℕ) (Q u : E → ℂ)
    (hQ : ContDiff ℝ ∞ Q) (hu : ContDiff ℝ ∞ u) (x : E)
    (hs : stationarySimilarityDefect a b m Q x=0) (hne : Q x≠0) :
    similarityLinearization a b m Q (fun y => Q y*u y) x =
      Q x*(Complex.I*Δ u x-fderiv ℝ u x ((1/2 : ℝ) • x)+
        2*Complex.I*∑ j : Fin 12,
          (fderiv ℝ Q x (EuclideanSpace.basisFun (Fin 12) ℝ j)/Q x)*
            fderiv ℝ u x (EuclideanSpace.basisFun (Fin 12) ℝ j))-
      Complex.I*(oddPowerDerivative m (Q x) (Q x*u x)-
        oddPowerNonlinearity m (Q x)*u x) := by
…

Mentions: OAI.DefocusingNLS.stationarySimilarityDefect, OAI.DefocusingNLS.similarityLinearization, OAI.DefocusingNLS.oddPowerDerivative, OAI.DefocusingNLS.oddPowerNonlinearity

theorem OAI.DefocusingNLS.radialMatched_similarityLinearization line 68
def OAI.DefocusingNLS.gaugeWeightedLaplacian line 88
Source documentation
The complexification of the weighted scalar Laplace expression.
```
noncomputable def gaugeWeightedLaplacian (Q u : E → ℂ) (x : E) : ℂ :=
…
```
def OAI.DefocusingNLS.gaugeTransport line 94
Source documentation
The complexification of the real transport expression in the profile gauge.
```
noncomputable def gaugeTransport (Q u : E → ℂ) (x : E) : ℂ :=
…
```
theorem OAI.DefocusingNLS.similarityLinearization_splitGauge line 99
theorem OAI.DefocusingNLS.radialMatched_splitGauge line 139