ScalarBurstError.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The prescribed rational burst duration makes the scalar diffusion error strictly smaller than the detector's fixed observation gap.

theorem OAI.ForcedComputation.VelocityDetector.scalar_burst_error line 13

theorem OAI.ForcedComputation.VelocityDetector.scalar_burst_error_initial line 41

Source documentation

The same comparison includes all older injections through their small value at the start of this burst; no decomposition of the scalar is needed.

theorem scalar_burst_error_initial (C L n : ℕ)
    {a : ℝ → Plane → Plane} {h w v : ℝ → Plane → ℝ} {w₀ v₀ : Plane → ℝ}
    (hw : TorusScalarSolution (2 * (duration C L n : ℝ)) 1 a h w w₀)
    (hv : TorusScalarSolution (2 * (duration C L n : ℝ)) 1 a
      (fun t x => h t x - scalarLaplacian (v t) x) v v₀)
    (hlap : ∀ t ∈ Icc 0 (2 * (duration C L n : ℝ)), ∀ x,
      |scalarLaplacian (v t) x| ≤ (laplacianBound C L n : ℝ))
    {E : ℝ} (hinit : ∀ x, |w₀ x - v₀ x| ≤ E) :
    ∀ t ∈ Icc 0 (2 * (duration C L n : ℝ)), ∀ x,
      |w t x - v t x| < E + 1 / 16 := by
…

Mentions: OAI.ForcedComputation.VelocityDetector.TorusScalarSolution, OAI.ForcedComputation.VelocityDetector.duration, OAI.ForcedComputation.VelocityDetector.scalarLaplacian, OAI.ForcedComputation.VelocityDetector.laplacianBound