OAI/GroupTheory/PolycyclicRecognition/Algebra/L2LabelDistance.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Distance to a finite label set from one L2 approximation

The comparison uses any one label known on the fixed component. Its conclusion takes distance to the whole set and needs no selection of labels.

  1. theorem OAI.PolycyclicRecognition.lintegral_infDist_le_L2 line 21

    Source documentation

    An L2 approximation to one point of a set bounds the average distance to the whole set on a probability space.

    theorem lintegral_infDist_le_L2 (μ : Measure X) [IsProbabilityMeasure μ]
    (f : X → W) (v : Lp W 2 μ) {S : Set W} {w : W} (hw : w ∈ S)
    (hv : (v : X → W) =ᵐ[μ] fun x => f x - w) :
    ∫⁻ x, ENNReal.ofReal (infDist (f x) S) ∂μ ≤ ENNReal.ofReal ‖v‖ := by
…