SpectralGaugeClassicalFlux.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Divergence identities for the finite-pressure radial eigenvalue system.

def OAI.DefocusingNLS.spectralGaugeFirstFlux line 10
def OAI.DefocusingNLS.spectralGaugeSecondFlux line 13

theorem OAI.DefocusingNLS.spectralGaugeClassicalFlux line 17

Source documentation

Differentiating the two actual fluxes gives precisely the weak-system sources.

theorem spectralGaugeClassicalFlux (μ A : ℝ → ℝ) (f g : ℝ → ℂ)
    (r dμ c : ℝ) (η lam pressure : ℂ) (hr : r ≠ 0) (hμn : μ r ≠ 0)
    (hμ : HasDerivAt μ dμ r)
    (hA : HasDerivAt A (c*μ r-11/r*A r) r)
    (hf : DifferentiableAt ℝ f r) (hg : DifferentiableAt ℝ g r)
    (hdf : DifferentiableAt ℝ (deriv f) r) (hdg : DifferentiableAt ℝ (deriv g) r)
    (heF : lam*f r=-(deriv (deriv g) r+
      (11/(r : ℂ)+(dμ : ℂ)/(μ r : ℂ))*deriv g r-η/(r : ℂ)^2*g r)-
        (A r : ℂ)/(μ r : ℂ)*deriv f r)
    (heG : lam*g r=deriv (deriv f) r+
      (11/(r : ℂ)+(dμ : ℂ)/(μ r : ℂ))*deriv f r-η/(r : ℂ)^2*f r-
        (A r : ℂ)/(μ r : ℂ)*deriv g r-pressure*f r) :
…