HomogeneousMildEnergy.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Exact energy identity for forced mild evolution

The identity is proved in the interaction picture and therefore holds for arbitrary Y data and continuous Y forcing. No generator-domain assumption or extra pair of spatial derivatives is needed.

theorem OAI.DefocusingNLS.forced_component_energy_derivative line 20

theorem OAI.DefocusingNLS.hasDerivAt_homogeneousForcedEnergy line 70

Source documentation

The two free rates and the exact real forcing pairing, valid for arbitrary mild data in the faithful homogeneous Hilbert space.

theorem hasDerivAt_homogeneousForcedEnergy (a b k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k)
    (f : HomogeneousY a k) (r : ℝ → HomogeneousY a k) (hr : Continuous r) (t : ℝ) :
    HasDerivAt (fun τ => ‖homogeneousForcedTrajectory a b k ha ha1 hk f r τ‖ ^ 2)
      (-a * ‖homogeneousLowEnergy a k ha1 hk
          (homogeneousForcedTrajectory a b k ha ha1 hk f r t)‖ ^ 2 +
        (6 - 2 * a - k) * ‖homogeneousHighEnergy a k ha1 hk
          (homogeneousForcedTrajectory a b k ha ha1 hk f r t)‖ ^ 2 +
        2 * inner ℝ (homogeneousForcedTrajectory a b k ha ha1 hk f r t) (r t)) t := by
…

Mentions: OAI.DefocusingNLS.HomogeneousY, OAI.DefocusingNLS.homogeneousForcedTrajectory, OAI.DefocusingNLS.homogeneousLowEnergy, OAI.DefocusingNLS.homogeneousHighEnergy

theorem OAI.DefocusingNLS.homogeneousForcedEnergy_balance line 94

Source documentation

Integrated energy balance for the actual forced evolution.

theorem homogeneousForcedEnergy_balance (a b k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k)
    (f : HomogeneousY a k) (r : ℝ → HomogeneousY a k) (hr : Continuous r) (t : ℝ) :
    ‖homogeneousForcedTrajectory a b k ha ha1 hk f r t‖ ^ 2 = ‖f‖ ^ 2 +
      ∫ τ in (0 : ℝ)..t,
        -a * ‖homogeneousLowEnergy a k ha1 hk
          (homogeneousForcedTrajectory a b k ha ha1 hk f r τ)‖ ^ 2 +
        (6 - 2 * a - k) * ‖homogeneousHighEnergy a k ha1 hk
          (homogeneousForcedTrajectory a b k ha ha1 hk f r τ)‖ ^ 2 +
        2 * inner ℝ (homogeneousForcedTrajectory a b k ha ha1 hk f r τ) (r τ) := by
…

Mentions: OAI.DefocusingNLS.HomogeneousY, OAI.DefocusingNLS.homogeneousForcedTrajectory, OAI.DefocusingNLS.homogeneousLowEnergy, OAI.DefocusingNLS.homogeneousHighEnergy