OAI/GroupTheory/PolycyclicRecognition/Analysis/NormalizedCellDomination.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.normalized_cell_transport_domination line 16

   Source documentation

   If the inverse image of the smaller cell lies in the sampling cell, the pushed normalized sampling law dominates its normalized restriction. The loss is exactly the ratio of the two Haar volumes.

   theorem normalized_cell_transport_domination
       {X : Type*} [MeasurableSpace X] (μ : Measure X)
       (C D : Set X) (hC : MeasurableSet C)
       (hC0 : μ C ≠ 0) (hCfin : μ C ≠ ∞)
       (hD0 : μ D ≠ 0) (hDfin : μ D ≠ ∞)
       (τ : X → X) (hτ : MeasurePreserving τ μ μ)
       (hcover : τ ⁻¹' C ⊆ D)
       (S : Set X) (hS : MeasurableSet S) :
       (cellProbabilityMeasure μ C hC0 hCfin : Measure X) S ≤
         (μ D / μ C) * (cellProbabilityMeasure μ D hD0 hDfin : Measure X) (τ ⁻¹' S) := by
   …

   Mentions: OAI.PolycyclicRecognition.cellProbabilityMeasure