production module

`AutoSamplingTheory.TechnicalLemmas.Measure.CommonMassSliceFamily`

5 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/Measure/CommonMassSliceFamily.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.Measure.CommonMassSliceAutoSamplingTheory.TechnicalLemmas.Measure.CommonRemovableMass

Imported by

AutoSamplingTheory.TechnicalLemmas.MeasureAutoSamplingTheory.TechnicalLemmas.Measure.CommonSlicePermutationReplacementAutoSamplingTheory.TechnicalLemmas.Measure.StrictCycleCheaperLocalReplacementTests.CommonMassSliceFamily

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

def AutoSamplingTheory.TechnicalLemmas.Measure.CommonMassSliceFamily.commonMassSliceFamily Partial Not mapped

No declaration docstring.

noncomputable def commonMassSliceFamily {n : ℕ}
    (mu : Fin (n + 1) → FiniteMeasure X) (i : Fin (n + 1)) :
    FiniteMeasure X :=
  commonMassSlice (commonRemovableMass mu) (mu i)

AutoSamplingTheory/TechnicalLemmas/Measure/CommonMassSliceFamily.lean:30published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.CommonMassSliceFamily.commonMassSliceFamily_mass Partial Not mapped

No declaration docstring.

theorem commonMassSliceFamily_mass {n : ℕ}
    (mu : Fin (n + 1) → FiniteMeasure X)
    (hpos : ∀ i, 0 < (mu i).mass) (i : Fin (n + 1)) :
    (commonMassSliceFamily mu i).mass = commonRemovableMass mu := by
  exact commonMassSlice_mass _ _ (hpos i)

AutoSamplingTheory/TechnicalLemmas/Measure/CommonMassSliceFamily.lean:35published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.CommonMassSliceFamily.commonMassSliceFamily_toMeasure_le Partial Not mapped

No declaration docstring.

theorem commonMassSliceFamily_toMeasure_le {n : ℕ}
    (mu : Fin (n + 1) → FiniteMeasure X)
    (hpos : ∀ i, 0 < (mu i).mass) (i : Fin (n + 1)) :
    ((commonMassSliceFamily mu i : FiniteMeasure X) : Measure X) ≤
      (mu i : Measure X) := by
  exact commonMassSlice_toMeasure_le _ _ (hpos i) (commonRemovableMass_le mu i)

AutoSamplingTheory/TechnicalLemmas/Measure/CommonMassSliceFamily.lean:41published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.CommonMassSliceFamily.commonMassSliceFamily_mass_pos Partial Not mapped

No declaration docstring.

theorem commonMassSliceFamily_mass_pos {n : ℕ}
    (mu : Fin (n + 1) → FiniteMeasure X)
    (hpos : ∀ i, 0 < (mu i).mass) (i : Fin (n + 1)) :
    0 < (commonMassSliceFamily mu i).mass := by
  rw [commonMassSliceFamily_mass mu hpos i]
  exact commonRemovableMass_pos mu hpos

AutoSamplingTheory/TechnicalLemmas/Measure/CommonMassSliceFamily.lean:48published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.CommonMassSliceFamily.commonMassSliceFamily_mass_eq Partial Not mapped

No declaration docstring.

theorem commonMassSliceFamily_mass_eq {n : ℕ}
    (mu : Fin (n + 1) → FiniteMeasure X)
    (hpos : ∀ i, 0 < (mu i).mass) (i j : Fin (n + 1)) :
    (commonMassSliceFamily mu i).mass = (commonMassSliceFamily mu j).mass := by
  rw [commonMassSliceFamily_mass mu hpos i,
    commonMassSliceFamily_mass mu hpos j]

end

end CommonMassSliceFamily
end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure/CommonMassSliceFamily.lean:55published source at 0e31a3cda412