production module

`AutoSamplingTheory.TechnicalLemmas.Measure.FiniteRemainder`

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

Imports

Mathlib.MeasureTheory.Measure.FiniteMeasure externalMathlib.MeasureTheory.Measure.Sub external

Imported by

AutoSamplingTheory.TechnicalLemmas.MeasureAutoSamplingTheory.TechnicalLemmas.Measure.CanonicalGlobalCompetitorTests.FiniteRemainder

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

def AutoSamplingTheory.TechnicalLemmas.Measure.FiniteRemainder.finiteRemainder Partial Not mapped

- The finite remainder left after removing a finite measure from an ambient finite measure. The definition makes sense without a domination hypothesis; exact reconstruction uses domination below.

noncomputable def finiteRemainder
    (ambient removed : FiniteMeasure X) : FiniteMeasure X :=
  ⟨(ambient : Measure X) - (removed : Measure X), by infer_instance⟩

@[simp]

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

theorem AutoSamplingTheory.TechnicalLemmas.Measure.FiniteRemainder.finiteRemainder_toMeasure Partial Not mapped

No declaration docstring.

theorem finiteRemainder_toMeasure
    (ambient removed : FiniteMeasure X) :
    (finiteRemainder ambient removed : Measure X) =
      (ambient : Measure X) - (removed : Measure X) :=
  rfl

/-- A dominated removed finite measure can be added back to its canonical
remainder to recover the ambient finite measure exactly. -/

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

theorem AutoSamplingTheory.TechnicalLemmas.Measure.FiniteRemainder.finiteRemainder_add_removed_eq Partial Not mapped

- A dominated removed finite measure can be added back to its canonical remainder to recover the ambient finite measure exactly.

theorem finiteRemainder_add_removed_eq
    (ambient removed : FiniteMeasure X)
    (hle : (removed : Measure X) ≤ (ambient : Measure X)) :
    finiteRemainder ambient removed + removed = ambient := by
  apply FiniteMeasure.toMeasure_injective
  change ((ambient : Measure X) - (removed : Measure X)) +
      (removed : Measure X) = (ambient : Measure X)
  exact Measure.sub_add_cancel_of_le hle

/-- Orientation consumed directly by the replacement-competitor algebra. -/

AutoSamplingTheory/TechnicalLemmas/Measure/FiniteRemainder.lean:43published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.FiniteRemainder.ambient_eq_finiteRemainder_add_removed Partial Not mapped

- Orientation consumed directly by the replacement-competitor algebra.

theorem ambient_eq_finiteRemainder_add_removed
    (ambient removed : FiniteMeasure X)
    (hle : (removed : Measure X) ≤ (ambient : Measure X)) :
    ambient = finiteRemainder ambient removed + removed := by
  exact (finiteRemainder_add_removed_eq ambient removed hle).symm

/-- Existence form: every dominated finite block admits an explicit additive
remainder decomposition. -/

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

theorem AutoSamplingTheory.TechnicalLemmas.Measure.FiniteRemainder.exists_finiteRemainder_of_le Partial Not mapped

- Existence form: every dominated finite block admits an explicit additive remainder decomposition.

theorem exists_finiteRemainder_of_le
    (ambient removed : FiniteMeasure X)
    (hle : (removed : Measure X) ≤ (ambient : Measure X)) :
    ∃ remainder : FiniteMeasure X, ambient = remainder + removed := by
  exact ⟨finiteRemainder ambient removed,
    ambient_eq_finiteRemainder_add_removed ambient removed hle⟩

end

end FiniteRemainder
end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure/FiniteRemainder.lean:61published source at 0e31a3cda412