OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingBlowupClock.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DefocusingNLS.expanding_clock_denominator_pos_of_lt line 11
2. theorem OAI.DefocusingNLS.expandingInverseClock_nonneg line 25
3. theorem OAI.DefocusingNLS.expandingInverseClock_eq_similarityTime line 32
4. theorem OAI.DefocusingNLS.expandingInverseClock_tendsto line 50
5. theorem OAI.DefocusingNLS.expanding_rescaled_amplitude line 56
6. theorem OAI.DefocusingNLS.expanding_rescaled_observation line 73
7. theorem OAI.DefocusingNLS.expanding_rescaled_observation_limit line 84

   Source documentation

   The rescaled modulus limit required in the main theorem follows from the similarity observation limit.

   theorem expanding_rescaled_observation_limit (a b L : ℝ) (hL : 0 < L)
       (g : ℝ → ℂ) (c : ℂ) (hg : Tendsto g atTop (𝓝 c)) :
       Tendsto (fun t => (L ^ (-2 : ℝ) - t) ^ a *
         ‖expandingPhysicalAmplitude a b L (expandingInverseClock L t) *
           g (expandingInverseClock L t)‖)
         (𝓝[<] (L ^ (-2 : ℝ))) (𝓝 ‖c‖) := by
   …

   Mentions: OAI.DefocusingNLS.expandingPhysicalAmplitude, OAI.DefocusingNLS.expandingInverseClock