OAI/MeasureTheory/Falconer/Measures/BorelProductPartition.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite disjoint Borel products in the original ambient space

  1. def OAI.Falconer.HasBorelProductPartition line 12

    Source documentation

    The finite partition used by the graph regularization, with its actual cardinality.

    def HasBorelProductPartition {d : ℕ} (S : Set (Space d × Space d)) (K : ℝ) : Prop :=
…

    Mentions: OAI.Falconer.Space

  2. theorem OAI.Falconer.HasBorelProductPartition.mono_bound line 18
  3. theorem OAI.Falconer.borel_product_partition_of_finset line 24
  4. theorem OAI.Falconer.borel_product_partition_single line 48