OAI/MathematicalPhysics/DefocusingNLS/Linear/SobolevConjugation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Complex conjugation in the Fourier Sobolev model

  1. def OAI.DefocusingNLS.fourierConjugate line 12

    Source documentation

    Conjugating a torus function conjugates its coefficients and reverses frequency.

    Distinct definitions of this name: ComparatorChallenges/DefocusingNLS.lean:111 (same statement text; different proof or body). Qualify references as OAI.DefocusingNLS.fourierConjugate@path.

    noncomputable def fourierConjugate (f : FourierL2) : FourierL2 :=
…

    Mentions: OAI.DefocusingNLS.FourierL2

  2. theorem OAI.DefocusingNLS.fourierConjugate_apply line 19
  3. theorem OAI.DefocusingNLS.fourierConjugate_involutive line 22
  4. theorem OAI.DefocusingNLS.fourierConjugate_norm line 27
  5. def OAI.DefocusingNLS.sobolevConjugation line 37

    Source documentation

    Conjugation of torus functions is a continuous real-linear map on H^k.

    noncomputable def sobolevConjugation : FourierL2 →L[ℝ] FourierL2 :=
…

    Mentions: OAI.DefocusingNLS.FourierL2

  6. theorem OAI.DefocusingNLS.sobolevConjugation_apply line 44
  7. theorem OAI.DefocusingNLS.sobolevFourierCoefficient_conjugate line 47
  8. theorem OAI.DefocusingNLS.frequencyCoordinates_neg line 53
  9. theorem OAI.DefocusingNLS.torusCharacter_neg line 59
  10. theorem OAI.DefocusingNLS.sobolevTorusFunction_conjugate line 65