PartitionLabel.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem356.FiniteCells.cellLabel line 15
Source documentation
The exact label of a point in a disjoint family; points outside all cells are assigned none, without choosing an arbitrary distinguished cell.
```
def cellLabel {X : Type uX} {ι : Type uIndex} (A : ι → Set X) (x : X) : Option ι :=
…
```
lemma OAI.Problem356.FiniteCells.cellLabel_eq_some_iff line 20
lemma OAI.Problem356.FiniteCells.cellLabel_eq_none_iff line 38
lemma OAI.Problem356.FiniteCells.cellLabel_fiber_some line 47
lemma OAI.Problem356.FiniteCells.cellLabel_fiber_none line 53
lemma OAI.Problem356.FiniteCells.measurable_cellLabel line 58

lemma OAI.Problem356.FiniteCells.map_cellLabel_eq_of_cell_masses line 75

Source documentation

Equal source cell masses give equal laws of the exact label, provided both measures are concentrated on the union of the cells.

lemma map_cellLabel_eq_of_cell_masses {X : Type uX} {ι : Type uIndex} [MeasurableSpace X]
    [MeasurableSpace (Option ι)] [MeasurableSingletonClass (Option ι)] [Countable ι]
    {μ ν : Measure X} {A : ι → Set X}
    (hA : ∀ i, MeasurableSet (A i))
    (hDisjoint : Pairwise (fun i j => Disjoint (A i) (A j)))
    (hμ : μ (⋃ i, A i)ᶜ = 0) (hν : ν (⋃ i, A i)ᶜ = 0)
    (hmass : ∀ i, μ (A i) = ν (A i)) :
    Measure.map (cellLabel A) μ = Measure.map (cellLabel A) ν := by
…

Mentions: OAI.Problem356.FiniteCells.cellLabel