OAI/GroupTheory/PolycyclicRecognition/Analysis/SectionVolume.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_section_measure_gt line 14

   Source documentation

   Fubini gives a large section without choosing a measurable family of representatives for the image of the parameter set.

   theorem exists_section_measure_gt
       {V Z : Type*} [MeasurableSpace V] [MeasurableSpace Z]
       (μ : Measure V) (ν : Measure Z) [SFinite μ] [SFinite ν]
       {K : Set (V × Z)} (hK : MeasurableSet K)
       {Q : Set Z} (hQ : MeasurableSet Q)
       (hKQ : ∀ p ∈ K, p.2 ∈ Q) (t : ℝ≥0∞)
       (hmass : t * ν Q < (μ.prod ν) K) :
       ∃ z ∈ Q, t < μ {v | (v, z) ∈ K} := by
   …