OAI/MathematicalPhysics/DefocusingNLS/Certificates/HorizontalHomogeneity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Removing the unit-vector normalization from the horizontal estimate

  1. theorem OAI.DefocusingNLS.horizontalDifference_mul line 11
  2. theorem OAI.DefocusingNLS.horizontalState_mul line 17
  3. theorem OAI.DefocusingNLS.horizontalIncrementSum_mul line 27
  4. theorem OAI.DefocusingNLS.horizontalFormAt_mul line 36
  5. theorem OAI.DefocusingNLS.horizontalForm_positive_of_unit_sphere line 43

    Source documentation

    Homogeneity extends the compact unit-sphere estimate to every nonzero jet.

    theorem horizontalForm_positive_of_unit_sphere (ell : ℕ) (τ σ b Z : ℝ)
    (hunit : ∀ B C : ℂ, (B, C) ∈ sphere (0 : ℂ × ℂ) 1 →
      0 < horizontalFormAt ell (τ, σ, b, Z, B, C))
    (B C : ℂ) (hBC : B ≠ 0 ∨ C ≠ 0) :
    0 < horizontalFormAt ell (τ, σ, b, Z, B, C) := by
…

    Mentions: OAI.DefocusingNLS.horizontalFormAt