`BookProof.DampedOscillatorEnergy.total_probability_conserved` {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] {T : Ω → Ω} (hT : Measurable T) : (μ.map T)

Initializing...

`BookProof.DampedOscillatorEnergy.total_probability_conserved` {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] {T : Ω → Ω} (hT : Measurable T) : (μ.map T) · Prove2Me