OAI/Analysis/FiniteFactor/OrbitSampling/RotationTransport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.coordinateRotate_neg_cube line 10
2. theorem OAI.FiniteFactor.coordinateRotate_phase line 21
3. theorem OAI.FiniteFactor.coordinateRotate_neg_phase line 28
4. theorem OAI.FiniteFactor.sourceSamplingHaar_rotate_withDensity line 38

   Source documentation

   Change of variables for an actual weighted Haar law. The inverse identity is needed only on the conull cube of representatives.

   theorem sourceSamplingHaar_rotate_withDensity (θ : SourceCoordinate → ℝ) (n : ℤ)
       (w : (SourceCoordinate → ℝ) → ℝ≥0∞) (hw : Measurable w) :
       (sourceSamplingHaar.withDensity w).map (coordinateRotate θ n) =
         sourceSamplingHaar.withDensity (fun y => w (coordinateRotate θ (-n) y)) := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.coordinateRotate