Documentation

TauCeti.MeasureTheory.Constructions.UnitInterval

The equipartition of the unit interval into m cells #

unitInterval.cellIdx m x is the index of the cell containing x when [0, 1] is cut into m pieces of equal length,

[0, 1/m), [1/m, 2/m), …, [(m-1)/m, 1].

The cells are the fibres of cellIdx m, and each has volume 1/m. This is the measure-theoretic content behind reading a finite object as an object on the canonical carrier (I, volume): a finite graph as a step graphon, a finite partition as a measurable one, an m-point law as a law on the unit interval.

The clipping at the top #

cellIdx m x = min ⌊m * x⌋₊ (m - 1). The min is what closes the top cell: without it x = 1 would be a fibre of its own and the fibres would no longer be m sets of equal measure. Clipping, rather than special-casing x = 1, also keeps the definition total in m: at m = 0 it returns 0, but that value has no cell-index meaning; results that interpret it as a valid cell index or compute a cell volume carry positivity or range hypotheses.

So the fibres are the half-open cells [i/m, (i+1)/m) for i + 1 < m, together with the closed top cell [(m-1)/m, 1] = Set.Ici ((m-1)/m).

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.unitInterval.cellIdx (m : ℕ) (x : ↑unitInterval) :
ℕ

The index of the cell containing x for the partition of [0, 1] into the m equal cells [0, 1/m), [1/m, 2/m), …, [(m-1)/m, 1].

The min closes the top cell, so that x = 1 is not a fibre of its own; see the module docstring. At m = 0 the value is 0 and carries no cell-index meaning; results that interpret the value as a valid cell index or compute cell volume require positivity or range hypotheses.

Equations
Instances For
    source
    theorem TauCeti.unitInterval.cellIdx_lt {m : ℕ} (hm : 0 < m) (x : ↑unitInterval) :
    cellIdx m x < m

    The cell index is a valid index into Fin m.

    source
    @[simp]
    theorem TauCeti.unitInterval.cellIdx_eq_iff_of_succ_lt {m i : ℕ} (hi : i + 1 < m) (x : ↑unitInterval) :
    cellIdx m x = i ↔ ↑i / ↑m ≤ ↑x ∧ ↑x < (↑i + 1) / ↑m

    A cell below the top one has the half-open fibre: cellIdx m x = i exactly when i / m ≤ x < (i + 1) / m.

    source
    @[simp]
    theorem TauCeti.unitInterval.cellIdx_eq_sub_one_iff {m : ℕ} (hm : 0 < m) (x : ↑unitInterval) :
    cellIdx m x = m - 1 ↔ ↑(m - 1) / ↑m ≤ ↑x

    The top cell is closed at 1: cellIdx m x = m - 1 exactly when (m - 1) / m ≤ x.

    source
    theorem TauCeti.unitInterval.measurable_cellIdx {m : ℕ} :
    Measurable (cellIdx m)

    The cell index depends measurably on the point.

    source
    theorem TauCeti.unitInterval.measurableSet_preimage_cellIdx (m i : ℕ) :
    MeasurableSet (cellIdx m ⁻¹' {i})

    Each cell is measurable.

    source
    theorem TauCeti.unitInterval.volume_preimage_cellIdx {m i : ℕ} (hi : i < m) :
    MeasureTheory.volume (cellIdx m ⁻¹' {i}) = (↑m)⁻¹

    Every cell of the m-fold equipartition has volume 1/m: the half-open [i/m, (i+1)/m) below the top cell, and the closed [(m-1)/m, 1] at the top.

    source
    noncomputable def TauCeti.unitInterval.cellFin (m : ℕ) [NeZero m] (x : ↑unitInterval) :
    Fin m

    The index of the cell containing x, as an element of Fin m. Positivity of m, carried by NeZero, is what makes cellIdx m x a valid index.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.unitInterval.coe_cellFin {m : ℕ} [NeZero m] (x : ↑unitInterval) :
      ↑(cellFin m x) = cellIdx m x
      source
      @[simp]
      theorem TauCeti.unitInterval.preimage_cellFin_singleton {m : ℕ} [NeZero m] (i : Fin m) :
      cellFin m ⁻¹' {i} = cellIdx m ⁻¹' {↑i}

      The cells of cellFin are those of cellIdx.

      source
      theorem TauCeti.unitInterval.measurable_cellFin {m : ℕ} [NeZero m] :
      Measurable (cellFin m)

      The Fin m-valued cell index depends measurably on the point.

      source
      theorem TauCeti.unitInterval.measurePreserving_cellFin {m : ℕ} [NeZero m] :
      MeasureTheory.MeasurePreserving (cellFin m) MeasureTheory.volume (ProbabilityTheory.uniformOn Set.univ)

      The cells are equally likely. The Fin m-valued cell index is measure preserving from (I, volume) to the uniform probability measure on Fin m: this is how an object on m equally weighted points is read on the unit interval.

      source
      theorem TauCeti.unitInterval.integral_pi_comp_cellIdx_eq_inv_smul_sum {m : ℕ} {V : Type u_1} {E : Type u_2} [Fintype V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (hm : 0 < m) (f : (V → ℕ) → E) :
      (∫ (x : V → ↑unitInterval), f fun (v : V) => cellIdx m (x v) ∂MeasureTheory.Measure.pi fun (x : V) => MeasureTheory.volume) = (↑m ^ Fintype.card V)⁻¹ • ∑ ψ : V → Fin m, f fun (v : V) => ↑(ψ v)

      Independent uniform points, read through their cells. The integral of a function of the cell indices of #V independent uniform points on [0, 1] is the average of that function over all #V-tuples of cells.

      This is the transfer that turns an integral over the continuous carrier (I, volume) into a finite sum, and it is where the equal volume of the cells is consumed. The integrand's argument is ℕ-valued, so no 0 < m hypothesis is hidden in a Fin m-valued cell map; the sum on the right ranges over V → Fin m, which is where the finiteness lives.