OAI/MathematicalPhysics/DefocusingNLS/Certificates/CompactFamilyIntegral.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DefocusingNLS.hasDerivAt_compactFamily_integral line 16

   Source documentation

   A fixed compact support supplies the integrable local derivative bound.

   theorem hasDerivAt_compactFamily_integral (F Fd : ℝ → E → ℂ)
       (hF : Continuous (Function.uncurry F)) (hFd : Continuous (Function.uncurry Fd))
       (K : Set E) (hK : IsCompact K)
       (hzero : ∀ t x, x ∉ K → F t x = 0)
       (hdzero : ∀ t x, x ∉ K → Fd t x = 0)
       (hd : ∀ t x, HasDerivAt (fun s => F s x) (Fd t x) t) (t : ℝ) :
       HasDerivAt (fun s => ∫ x, F s x) (∫ x, Fd t x) t := by
   …

2. theorem OAI.DefocusingNLS.hasDerivAt_compactFamily_fourier line 56

   Source documentation

   The same local argument differentiates the physical Fourier transform.

   theorem hasDerivAt_compactFamily_fourier (F Fd : ℝ → E → ℂ)
       (hF : Continuous (Function.uncurry F)) (hFd : Continuous (Function.uncurry Fd))
       (K : Set E) (hK : IsCompact K)
       (hzero : ∀ t x, x ∉ K → F t x = 0)
       (hdzero : ∀ t x, x ∉ K → Fd t x = 0)
       (hd : ∀ t x, HasDerivAt (fun s => F s x) (Fd t x) t) (t : ℝ) (ξ : E) :
       HasDerivAt (fun s => radianFourierIntegral (F s) ξ)
         (radianFourierIntegral (Fd t) ξ) t := by
   …

   Mentions: OAI.DefocusingNLS.radianFourierIntegral