Partitions of the unit interval by groups of cells

A partition P of Fin m with 0 < m lifts to the partition P.cellPartition of the unit interval whose parts are the unions of the m equal cells over the parts of P, namely the fibres of x ↦ P.part (cellFin m x). Its parts are measurable and are exactly the cell preimages of the parts of P, and the part selected at x by its canonical index is the cell preimage of the part of P containing the cell of x.

Main definitions

• Finpartition.cellPartition: the partition of the unit interval induced by a partition of Fin m.

Main results

• Finpartition.mem_cellPartition_parts_iff: the parts are the cell preimages of the parts of P.
• Finpartition.coe_index_cellPartition: the part through a point.

noncomputable def Finpartition.cellPartition {m : ℕ} [NeZero m] (P : Finpartition Finset.univ) : Finpartition Set.univ

The partition of the unit interval obtained from a partition P of Fin m by grouping the m equal cells of I according to the parts of P.

theorem Finpartition.measurable_part_cellFin {m : ℕ} [NeZero m] (P : Finpartition Finset.univ) : Measurable fun (x : ↑unitInterval) => P.part (TauCeti.unitInterval.cellFin m x)

The part of P containing the cell of a point depends measurably on the point.

theorem Finpartition.measurableSet_of_mem_cellPartition {m : ℕ} [NeZero m] (P : Finpartition Finset.univ) (p : Set ↑unitInterval) : p ∈ P.cellPartition.parts → MeasurableSet p

The parts of P.cellPartition are measurable.

theorem Finpartition.preimage_part_cellFin_mem {m : ℕ} [NeZero m] (P : Finpartition Finset.univ) (x : ↑unitInterval) : TauCeti.unitInterval.cellFin m ⁻¹' ↑(P.part (TauCeti.unitInterval.cellFin m x)) ∈ P.cellPartition.parts

The cells of the part of P containing the cell of x form the part of P.cellPartition containing x.

theorem Finpartition.mem_cellPartition_parts_iff {m : ℕ} [NeZero m] (P : Finpartition Finset.univ) {s : Set ↑unitInterval} : s ∈ P.cellPartition.parts ↔ ∃ A ∈ P.parts, TauCeti.unitInterval.cellFin m ⁻¹' ↑A = s

The parts of P.cellPartition are exactly the unions of the cells over the parts of P.

@[simp]

theorem Finpartition.coe_index_cellPartition {m : ℕ} [NeZero m] (P : Finpartition Finset.univ) (x : ↑unitInterval) : ↑(P.cellPartition.indexedPartition.index x) = TauCeti.unitInterval.cellFin m ⁻¹' ↑(P.part (TauCeti.unitInterval.cellFin m x))

The part through a point. The part of P.cellPartition that its canonical index selects at x is the union of the cells over the part of P containing the cell of x.