FiniteMassSplit.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem356.continuous_real_cumulative line 15

Source documentation

The cumulative mass of a finite real measure with null singletons is continuous.

theorem continuous_real_cumulative (μ : Measure ℝ) [IsFiniteMeasure μ]
    [NullSingletonClass μ] : Continuous (fun t : ℝ => μ.real (Iic t)) := by
…

theorem OAI.Problem356.exists_real_cumulative_eq line 26

Source documentation

Every strictly intermediate mass is the mass of a lower interval.

theorem exists_real_cumulative_eq (μ : Measure ℝ) [IsFiniteMeasure μ]
    [NullSingletonClass μ] {r : ℝ} (hr : 0 < r) (hrμ : r < μ.real univ) :
    ∃ t : ℝ, μ.real (Iic t) = r := by
…

theorem OAI.Problem356.exists_measurable_subset_measure_eq line 41

Source documentation

A finite measure with null singletons on a standard Borel space can realize any prescribed mass inside any measurable set.

theorem exists_measurable_subset_measure_eq {α : Type uAlpha} [MeasurableSpace α]
    [StandardBorelSpace α] (μ : Measure α) [IsFiniteMeasure μ]
    [NullSingletonClass μ] {A : Set α} (hA : MeasurableSet A)
    {r : ℝ≥0∞} (hr : r ≤ μ A) :
    ∃ B : Set α, MeasurableSet B ∧ B ⊆ A ∧ μ B = r := by
…

theorem OAI.Problem356.exists_fin_disjoint_subsets_measure line 80

Source documentation

Finitely many prescribed masses whose total does not exceed the mass of a measurable set can be realized by pairwise disjoint measurable subsets.

theorem exists_fin_disjoint_subsets_measure {α : Type uAlpha} [MeasurableSpace α]
    [StandardBorelSpace α] (μ : Measure α) [IsFiniteMeasure μ]
    [NullSingletonClass μ] {n : ℕ} (q : Fin n → ℝ≥0∞)
    {A : Set α} (hA : MeasurableSet A) (hq : ∑ i, q i ≤ μ A) :
    ∃ B : Fin n → Set α,
      (∀ i, MeasurableSet (B i)) ∧ (∀ i, B i ⊆ A) ∧
      Pairwise (fun i j => Disjoint (B i) (B j)) ∧ (∀ i, μ (B i) = q i) := by
…

theorem OAI.Problem356.exists_finite_disjoint_subsets_measure line 115

Source documentation

Fintype-indexed version of finite prescribed-mass splitting.

theorem exists_finite_disjoint_subsets_measure {α : Type uAlpha} {ι : Type uIndex} [MeasurableSpace α]
    [StandardBorelSpace α] [Fintype ι] (μ : Measure α) [IsFiniteMeasure μ]
    [NullSingletonClass μ] (q : ι → ℝ≥0∞)
    {A : Set α} (hA : MeasurableSet A) (hq : ∑ i, q i ≤ μ A) :
    ∃ B : ι → Set α,
      (∀ i, MeasurableSet (B i)) ∧ (∀ i, B i ⊆ A) ∧
      Pairwise (fun i j => Disjoint (B i) (B j)) ∧ (∀ i, μ (B i) = q i) := by
…

theorem OAI.Problem356.exists_finite_mass_partition_ae line 136

Source documentation

When prescribed masses exhaust the source mass, the disjoint subsets cover it up to a null remainder. Empty index types are allowed.

theorem exists_finite_mass_partition_ae {α : Type uAlpha} {ι : Type uIndex} [MeasurableSpace α]
    [StandardBorelSpace α] [Fintype ι] (μ : Measure α) [IsFiniteMeasure μ]
    [NullSingletonClass μ] (q : ι → ℝ≥0∞)
    {A : Set α} (hA : MeasurableSet A) (hq : ∑ i, q i = μ A) :
    ∃ B : ι → Set α,
      (∀ i, MeasurableSet (B i)) ∧ (∀ i, B i ⊆ A) ∧
      Pairwise (fun i j => Disjoint (B i) (B j)) ∧
      (∀ i, μ (B i) = q i) ∧ μ (A \ ⋃ i, B i) = 0 := by
…