AutoSamplingTheory.TechnicalLemmas.Measure.CommonRemovableMass

- Minimum total mass among a nonempty finite family of local measures.

noncomputable def commonRemovableMass {n : ℕ}
    (mu : Fin (n + 1) → FiniteMeasure X) : ℝ≥0 :=
  ⨅ i, (mu i).mass

/-- The common removable mass is bounded above by every local total mass. -/

AutoSamplingTheory/TechnicalLemmas/Measure/CommonRemovableMass.lean:32published source at 0e31a3cda412

- The common removable mass is bounded above by every local total mass.

theorem commonRemovableMass_le {n : ℕ}
    (mu : Fin (n + 1) → FiniteMeasure X) (i : Fin (n + 1)) :
    commonRemovableMass mu ≤ (mu i).mass := by
  unfold commonRemovableMass
  exact Finite.ciInf_le (fun j : Fin (n + 1) => (mu j).mass) i

/-- One local piece attains the common removable mass. -/

AutoSamplingTheory/TechnicalLemmas/Measure/CommonRemovableMass.lean:37published source at 0e31a3cda412

- One local piece attains the common removable mass.

theorem exists_mass_eq_commonRemovableMass {n : ℕ}
    (mu : Fin (n + 1) → FiniteMeasure X) :
    ∃ i : Fin (n + 1), (mu i).mass = commonRemovableMass mu := by
  obtain ⟨i, hi⟩ :=
    exists_eq_ciInf_of_finite (f := fun j : Fin (n + 1) => (mu j).mass)
  exact ⟨i, by simpa [commonRemovableMass] using hi⟩

/-- If every local finite measure has positive total mass, then their common
removable mass is positive. -/

AutoSamplingTheory/TechnicalLemmas/Measure/CommonRemovableMass.lean:44published source at 0e31a3cda412

- If every local finite measure has positive total mass, then their common removable mass is positive.

theorem commonRemovableMass_pos {n : ℕ}
    (mu : Fin (n + 1) → FiniteMeasure X)
    (hpos : ∀ i, 0 < (mu i).mass) :
    0 < commonRemovableMass mu := by
  obtain ⟨i, hi⟩ := exists_mass_eq_commonRemovableMass mu
  rw [← hi]
  exact hpos i

end

end CommonRemovableMass
end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure/CommonRemovableMass.lean:53published source at 0e31a3cda412