OriginalRecovery.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The original adjoint sum is estimated on every discarded set. The central sum enters only on the moving good set; its boundary error is averaged over the fixed common good set.

theorem OAI.LipschitzHilbert.three_term_norm line 16
theorem OAI.LipschitzHilbert.original_recovery_pointwise line 24
theorem OAI.LipschitzHilbert.original_recovery_integral line 55

theorem OAI.LipschitzHilbert.recover_constant_from_translation_average line 92

Source documentation

Averaging a pointwise recovery inequality does not require the moving exceptional sets themselves to be jointly measurable.

theorem recover_constant_from_translation_average (R P C : ℝ) (hR : 0 < R)
    (error : ℝ → ℝ) (herror : IntervalIntegrable error volume 0 R)
    (hbound : ∀ origin ∈ Icc 0 R, P ≤ C+error origin) :
    P ≤ C+(∫ origin in (0:ℝ)..R, error origin)/R := by
…

theorem OAI.LipschitzHilbert.recover_original_from_moving_good line 107

Source documentation

Fixed exceptions, each moving exception, the mask error, the averaged boundary error, and the central estimate bound the original sum.

theorem recover_original_from_moving_good
    (μ : Measure X) (F Z0 : Set X) (Z : ℝ → Set X)
    (hFm : MeasurableSet F) (hZ0m : MeasurableSet Z0)
    (hZm : ∀ origin, MeasurableSet (Z origin))
    (hZ0 : Z0 ⊆ F) (hZ : ∀ origin, Z origin ⊆ Z0)
    (P Q : X → E) (W : ℝ → X → E)
    (hP : IntegrableOn (fun x => ‖P x‖) F μ)
    (hPQ : IntegrableOn (fun x => ‖P x-Q x‖) Z0 μ)
    (hQW : ∀ origin, IntegrableOn (fun x => ‖Q x-W origin x‖) Z0 μ)
    (hW : ∀ origin, IntegrableOn (fun x => ‖W origin x‖) (Z origin) μ)
    (R Cfixed Cbad Cmask Cboundary Ccentral : ℝ) (hR : 0 < R)
    (hfixed : (∫ x in F\Z0, ‖P x‖ ∂μ) ≤ Cfixed)
…