OAI/GroupTheory/PolycyclicRecognition/Analysis/CellProbabilityTransport.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.map_cellProbabilityMeasure_of_image_ratio line 15

   Source documentation

   Equal relative masses of chart images identify the normalized sampling laws. This is used with the exact exponential-coordinate Jacobian.

   theorem map_cellProbabilityMeasure_of_image_ratio
       {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
       (μ : Measure X) (ν : Measure Y) (f : X → Y) (hf : Measurable f)
       (C : Set X) (hC0 : μ C ≠ 0) (hCfin : μ C ≠ ∞)
       (himage0 : ν (f '' C) ≠ 0) (himagefin : ν (f '' C) ≠ ∞)
       (hratio : ∀ A : Set X, (ν (f '' A)).toReal / (ν (f '' C)).toReal =
         (μ A).toReal / (μ C).toReal) :
       ProbabilityMeasure.map (cellProbabilityMeasure μ C hC0 hCfin) f =
         cellProbabilityMeasure ν (f '' C) himage0 himagefin := by
   …

   Mentions: OAI.PolycyclicRecognition.cellProbabilityMeasure