QuotientSectionIndependence.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The product Haar normalization is independent of the section

theorem OAI.PolycyclicRecognition.quotientSection_product_independent line 20

Source documentation

Changing the continuous quotient section translates each kernel fiber on the right. Thus one product normalization serves every adapted basis.

theorem quotientSection_product_independent
    (π : N →* Q) (hπ : Continuous π)
    (s t : C(Q, N)) (hs : ∀ q, π (s q) = q) (ht : ∀ q, π (t q) = q)
    (μQ : Measure Q) (μI : Measure π.ker) [SFinite μQ] [SFinite μI]
    [μI.IsMulRightInvariant] :
    Measure.map (quotientSectionHomeomorph π hπ s hs).symm (μQ.prod μI) =
      Measure.map (quotientSectionHomeomorph π hπ t ht).symm (μQ.prod μI) := by
…

Mentions: OAI.PolycyclicRecognition.quotientSectionHomeomorph