SchwartzSamplingContinuity.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Continuous sampling at a fixed period

The finite-jet estimate gives a continuous linear sampling map. Combining it with the exact dilation identity handles families at a changing physical scale.

theorem OAI.DefocusingNLS.physicalSampling_seminorm_bound line 18
def OAI.DefocusingNLS.physicalSchwartzTorusSamplingCLM line 37
theorem OAI.DefocusingNLS.physicalSchwartzTorusSamplingCLM_apply line 47

theorem OAI.DefocusingNLS.continuous_dilatedPhysicalSampling line 53

Source documentation

Changing period is reduced to period one after the physical dilation.

theorem continuous_dilatedPhysicalSampling {P : Type*} [TopologicalSpace P]
    (a k : ℝ) (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k)
    (L : P → {L : ℝ // 1 ≤ L}) (hL : Continuous L)
    (ψ : P → 𝓢(E, ℂ)) (hψ : Continuous ψ) :
    Continuous (fun t => schwartzTorusSample a k (L t).1 ha1 hk (L t).2
      (radianFourierKernel
        (schwartzPhysicalDilation a (L t).1
          (lt_of_lt_of_le zero_lt_one (L t).2) (ψ t)))) := by
…

Mentions: OAI.DefocusingNLS.schwartzTorusSample, OAI.DefocusingNLS.radianFourierKernel, OAI.DefocusingNLS.schwartzPhysicalDilation