OAI/Analysis/FiniteFactor/Sampling/SmoothingLaw.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.samplingBoundary line 11
2. theorem OAI.FiniteFactor.samplingBoundary_measurable line 14
3. theorem OAI.FiniteFactor.samplingBoundary_measure line 17
4. theorem OAI.FiniteFactor.samplingSmooth_indicator_error_le_one line 37
5. theorem OAI.FiniteFactor.samplingSmooth_expected_error line 48

   Source documentation

   The interval smoothing error integrated under any actual phase law with density bounded by two. Only one-dimensional domination is used.

   theorem samplingSmooth_expected_error (ν : Measure ℝ) [IsProbabilityMeasure ν]
       (hν : ν ≤ (2 : ℝ≥0∞) • unitIntervalMeasure) (H : ℕ) (hH : 0 < H)
       (a b δ : ℝ) (hδ : 0 < δ) :
       (∫ t, |samplingSmooth H (Set.Icc a b) t -
         (Set.Icc a b).indicator (fun _ => (1 : ℝ)) t| ∂ν) ≤
         12*δ + 1/(4*(H : ℝ)*δ^2) := by
   …

   Mentions: OAI.FiniteFactor.unitIntervalMeasure, OAI.FiniteFactor.samplingSmooth