production module

`AutoSamplingTheory.TechnicalLemmas.Measure.FiniteSumDomination`

3 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/Measure/FiniteSumDomination.lean.

Imports

Mathlib.Algebra.BigOperators.Group.Finset.Basic externalMathlib.MeasureTheory.Measure.FiniteMeasure external

Imported by

AutoSamplingTheory.TechnicalLemmas.MeasureAutoSamplingTheory.TechnicalLemmas.Measure.CanonicalGlobalCompetitorTests.FiniteSumDomination

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

theorem AutoSamplingTheory.TechnicalLemmas.Measure.FiniteSumDomination.toMeasure_finsetSum_le Partial Not mapped

No declaration docstring.

theorem toMeasure_finsetSum_le
    (s : Finset I) (mu nu : I → FiniteMeasure X)
    (hle : ∀ i, (mu i : Measure X) ≤ (nu i : Measure X)) :
    ((s.sum mu : FiniteMeasure X) : Measure X) ≤
      ((s.sum nu : FiniteMeasure X) : Measure X) := by
  classical
  induction s using Finset.induction_on with
  | empty => simp
  | @insert a s ha ih =>
      rw [Finset.sum_insert ha, Finset.sum_insert ha,
        FiniteMeasure.toMeasure_add, FiniteMeasure.toMeasure_add]
      exact add_le_add (hle a) ih

AutoSamplingTheory/TechnicalLemmas/Measure/FiniteSumDomination.lean:24published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.FiniteSumDomination.toMeasure_fintypeSum_le Partial Not mapped

No declaration docstring.

theorem toMeasure_fintypeSum_le
    [Fintype I] (mu nu : I → FiniteMeasure X)
    (hle : ∀ i, (mu i : Measure X) ≤ (nu i : Measure X)) :
    ((∑ i, mu i : FiniteMeasure X) : Measure X) ≤
      ((∑ i, nu i : FiniteMeasure X) : Measure X) := by
  classical
  exact toMeasure_finsetSum_le Finset.univ mu nu hle

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

theorem AutoSamplingTheory.TechnicalLemmas.Measure.FiniteSumDomination.toMeasure_fintypeSum_le_ambient Partial Not mapped

No declaration docstring.

theorem toMeasure_fintypeSum_le_ambient
    [Fintype I] (mu nu : I → FiniteMeasure X) (ambient : FiniteMeasure X)
    (hle : ∀ i, (mu i : Measure X) ≤ (nu i : Measure X))
    (hambient : ((∑ i, nu i : FiniteMeasure X) : Measure X) ≤
      (ambient : Measure X)) :
    ((∑ i, mu i : FiniteMeasure X) : Measure X) ≤
      (ambient : Measure X) := by
  exact (toMeasure_fintypeSum_le mu nu hle).trans hambient

end

end FiniteSumDomination
end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure/FiniteSumDomination.lean:45published source at 0e31a3cda412