OAI/Analysis/FiniteFactor/CrossedProduct/SmallPartitionSets.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteFactor.sourceSmallPartitionSet line 11
  2. theorem OAI.FiniteFactor.sourceSmallPartitionSet_measurable line 14
  3. theorem OAI.FiniteFactor.unitInterval_partition_unique line 18
  4. theorem OAI.FiniteFactor.sourceSmallPartition_indicator_sum line 35
  5. theorem OAI.FiniteFactor.sourceSmallPartitionSet_measure_le line 49

    Source documentation

    Every cell has mass at most 1/n under the actual product Haar measure.

    theorem sourceSmallPartitionSet_measure_le (n : ℕ) (_hn : 0 < n) (j : Fin n) :
    sourceSamplingHaar (sourceSmallPartitionSet n j) ≤ ENNReal.ofReal (1/(n : ℝ)) := by
…

    Mentions: OAI.FiniteFactor.sourceSamplingHaar, OAI.FiniteFactor.sourceSmallPartitionSet