CellOccupationError.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Finite-cell errors for occupation observables

The observable may vary with the scale. Only its common bound matters, so the estimate survives projection from nonunique factor coordinates.

theorem OAI.PolycyclicRecognition.norm_setIntegral_sub_le_symmDiff line 19

Source documentation

Changing a finite sampling cell changes a bounded observable integral by at most its bound times the measure of the symmetric difference.

theorem norm_setIntegral_sub_le_symmDiff
    {X E : Type*} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E]
    (μ : Measure X) {s t : Set X} (hs : MeasurableSet s) (ht : MeasurableSet t)
    (hfs : μ s < ⊤) (hft : μ t < ⊤)
    (f : X → E) (hf : AEStronglyMeasurable f μ)
    {C : ℝ} (hC : 0 ≤ C) (hb : ∀ x, ‖f x‖ ≤ C) :
    ‖(∫ x in s, f x ∂μ) - ∫ x in t, f x ∂μ‖ ≤ C * (μ (s ∆ t)).toReal := by
…

theorem OAI.PolycyclicRecognition.norm_cell_translation_integral_error_le line 53

Source documentation

A measure-preserving change of sampling coordinates has an error controlled solely by the symmetric difference of the finite cell.

theorem norm_cell_translation_integral_error_le
    {X : Type*} [MeasurableSpace X] (μ : Measure X)
    (T : X → X) (hT : MeasurePreserving T μ μ)
    {s : Set X} (hs : MeasurableSet s) (hfin : μ s < ⊤)
    (f : X → ℝ) (hf : AEStronglyMeasurable f μ)
    {C : ℝ} (hC : 0 ≤ C) (hb : ∀ x, ‖f x‖ ≤ C) :
    ‖(∫ x in s, f (T x) ∂μ) - ∫ x in s, f x ∂μ‖ ≤
      C * (μ ((T ⁻¹' s) ∆ s)).toReal := by
…

theorem OAI.PolycyclicRecognition.cell_translation_integral_error_tendsto_zero line 74

Source documentation

Vanishing boundary loss makes every uniformly bounded, scale-dependent sampling observable asymptotically translation invariant.

theorem cell_translation_integral_error_tendsto_zero
    {X ι : Type*} [MeasurableSpace X] (μ : Measure X)
    (T : ι → X → X) (hT : ∀ i, MeasurePreserving (T i) μ μ)
    {s : Set X} (hs : MeasurableSet s) (hfin : μ s < ⊤)
    (f : ι → X → ℝ) (hf : ∀ i, AEStronglyMeasurable (f i) μ)
    {C : ℝ} (hC : 0 ≤ C) (hb : ∀ i x, ‖f i x‖ ≤ C)
    {l : Filter ι}
    (hcell : Tendsto (fun i => μ (((T i) ⁻¹' s) ∆ s)) l (𝓝 0)) :
    Tendsto (fun i => (∫ x in s, f i (T i x) ∂μ) - ∫ x in s, f i x ∂μ)
      l (𝓝 0) := by
…