production module

`AutoSamplingTheory.TechnicalLemmas.Measure`

1 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/Measure.lean.

Imports

Imported by

AutoSamplingTheory.TechnicalLemmas

Placeholder scan

0 declaration(s) flagged

Gate status

Compiled

Declarations

theorem AutoSamplingTheory.TechnicalLemmas.Measure.integrable_of_measure_eq Compiled Not mapped

- Integrability is invariant under replacing the ambient measure by an equal measure.

theorem integrable_of_measure_eq
    {alpha eps : Type*} [MeasurableSpace alpha] [TopologicalSpace eps]
    [ContinuousENorm eps]
    {f : alpha -> eps} {mu nu : MeasureTheory.Measure alpha} (hmunu : mu = nu)
    (hf : MeasureTheory.Integrable f mu) :
    MeasureTheory.Integrable f nu := by
  simpa [hmunu] using hf

export AutoSamplingTheory (
  lawMapEqOfAEEq
  lawMapIntegral
  lawMapIntegralHasDerivAtOfSample
  lawIntegralHasDerivAtOfMeasureMapEqAndSample
  lawMapIntegralHasDerivAtOfDominated
  lawIntegralHasDerivAtOfMeasureMapEqAndDominated
  lawMapProdEqOfAEEq
  lawMapProdFst
  lawMapProdSnd
  lawMapProdSwap
  condDistribAeEqCondExpKernelMap
  condDistribIntegralSampleAeEqOfCondExpKernelMap
  condDistribIntegralAEStronglyMeasurable
  condDistribIntegralIntegrable
  condDistribIntegralMapAEStronglyMeasurable
  condDistribIntegralMapIntegrable
  condDistribIntegralMapIntegral
  condDistribIntegralNamedLawIntegral
  condDistribIntegralNamedLawAEStronglyMeasurable
  condDistribIntegralNamedLawIntegrable
  condDistribIntegralNamedFieldRegularity
)

end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure.lean:36published source at 77184245109a