OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialExteriorParameter.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Fixed-power continuity of the actual exterior expansion and residual coefficients.

  1. theorem OAI.DefocusingNLS.continuous_radialPolynomial_mul_coeff line 11
  2. theorem OAI.DefocusingNLS.continuous_radialPolynomial_pow_coeff line 19
  3. theorem OAI.DefocusingNLS.continuous_radialPolynomialPower_coeff line 28
  4. theorem OAI.DefocusingNLS.continuous_radialExteriorExpansion_coeff line 39
  5. theorem OAI.DefocusingNLS.continuous_radialExteriorResidual_coeff line 54
  6. theorem OAI.DefocusingNLS.radialExteriorExpansion_fixed_power_limit line 65
  7. theorem OAI.DefocusingNLS.radialExteriorBase_fixed_power_limit line 77
  8. theorem OAI.DefocusingNLS.radialExteriorResidual_degree line 86
  9. theorem OAI.DefocusingNLS.radialExteriorResidual_fixed_power_limit line 117
  10. theorem OAI.DefocusingNLS.radialExteriorSource_fixed_power_limit line 131