OAI/Probability/PosteriorReplicas/Measures/TiltNormalization.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PosteriorReplicas.bounded_withDensity_finite line 10
2. lemma OAI.PosteriorReplicas.tiltedFiber_probability line 17
3. lemma OAI.PosteriorReplicas.tiltMass_smul_tiltedFiber line 28
4. lemma OAI.PosteriorReplicas.pi_tiltMass_smul line 38
5. lemma OAI.PosteriorReplicas.weighted_fiber_pi_integral line 53
6. lemma OAI.PosteriorReplicas.equalLabelLeft_tilt line 66
7. lemma OAI.PosteriorReplicas.equalLabelRight_tilt line 79