OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Detector/DetectorBlockSum.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A detector's countably many bursts form a smooth field: only finitely many bursts have begun in a neighborhood of any physical time.

  1. def OAI.ForcedComputation.VelocityDetector.detectorBlockSum line 16
  2. theorem OAI.ForcedComputation.VelocityDetector.detectorBlockSum_local_of_time_bound line 19
  3. theorem OAI.ForcedComputation.VelocityDetector.detectorBlockSum_local line 34
  4. theorem OAI.ForcedComputation.VelocityDetector.detectorBlockSum_local_of_approximation line 44

    Source documentation

    A coarse rational approximation to physical time gives a finite prefix valid throughout a neighborhood, hence for every derivative there as well.

    theorem detectorBlockSum_local_of_approximation (F : ℕ → ℝ × Plane → E)
    (hbefore : ∀ (n : ℕ) y, y.1 < 2 * ((n : ℝ) + 1) → F n y = 0)
    (y : ℝ × Plane) (q : ℚ) (hq : |y.1 - (q : ℝ)| ≤ 1) :
    detectorBlockSum F =ᶠ[𝓝 y]
      fun z => ∑ n ∈ Finset.range ⌈q + 2⌉₊, F n z := by
…

    Mentions: OAI.ForcedComputation.VelocityDetector.detectorBlockSum

  5. theorem OAI.ForcedComputation.VelocityDetector.detectorBlockSum_smooth line 55