class GaudisCrypt.MeasureFree (α : Type u_1) : Prop

A type α is measure-free (Fremlin 438A: "measure-free" / "of measure zero", there stated for cardinals) if every probability measure on α defined on all subsets of α (i.e., w.r.t. the discrete σ-algebra ⊤) gives positive mass to some singleton.

• exists_pos_singleton (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] : ∃ (x : α), 0 < μ {x}

instance GaudisCrypt.MeasureFree.of_countable {α : Type u_1} [Countable α] : MeasureFree α

Every countable type is measure-free.

theorem GaudisCrypt.MeasureFree.exists_pos_singleton_of_ne_zero {α : Type u_1} [MeasureFree α] (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] (h : μ ≠ 0) : ∃ (x : α), 0 < μ {x}

On a measure-free type, every nonzero s-finite measure on the discrete σ-algebra gives positive mass to some singleton.

theorem GaudisCrypt.MeasureFree.eq_zero_of_forall_singleton {α : Type u_1} [MeasureFree α] (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] (h : ∀ (x : α), μ {x} = 0) : μ = 0

On a measure-free type, an s-finite measure on the discrete σ-algebra that vanishes on all singletons is zero.

theorem GaudisCrypt.MeasureFree.measure_eq_tsum_singleton {α : Type u_1} [MeasureFree α] (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] (A : Set α) : μ A = ∑' (x : ↑A), μ {↑x}

On a measure-free type, every s-finite measure on the discrete σ-algebra is discrete: the measure of a set is the sum of the masses of its points.

theorem GaudisCrypt.MeasureFree.of_injective {α : Type u_1} {β : Type u_2} [MeasureFree α] {f : β → α} (hf : Function.Injective f) : MeasureFree β

Measure-freeness passes to types that inject into a measure-free type.

theorem GaudisCrypt.MeasureFree.of_equiv {α : Type u_1} {β : Type u_2} [MeasureFree β] (e : α ≃ β) : MeasureFree α

Measure-freeness is invariant under equivalence.

instance GaudisCrypt.MeasureFree.subtype {α : Type u_1} [MeasureFree α] (p : α → Prop) : MeasureFree (Subtype p)

instance GaudisCrypt.MeasureFree.ulift {α : Type u_1} [MeasureFree α] : MeasureFree (ULift.{u_2, u_1} α)

instance GaudisCrypt.MeasureFree.sigma {ι : Type u_1} {α : ι → Type u_2} [MeasureFree ι] [∀ (i : ι), MeasureFree (α i)] : MeasureFree ((i : ι) × α i)

A sum of measure-free types indexed by a measure-free type is measure-free.

instance GaudisCrypt.MeasureFree.prod {α : Type u_1} {β : Type u_2} [MeasureFree α] [MeasureFree β] : MeasureFree (α × β)

instance GaudisCrypt.MeasureFree.sum {α : Type u} {β : Type v} [MeasureFree α] [MeasureFree β] : MeasureFree (α ⊕ β)

instance GaudisCrypt.MeasureFree.option {α : Type u_1} [MeasureFree α] : MeasureFree (Option α)

theorem GaudisCrypt.MeasureFree.of_le_aleph_one {α : Type u_1} (h : Cardinal.mk α ≤ Cardinal.aleph 1) : MeasureFree α

Every type of cardinality at most ℵ₁ is measure-free (Ulam; Fremlin 438C).