OAI/Probability/FreeIsing/Ising/CanonicalClippedWeight.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.ClippedArtanhWeight.weight_eq_stopped_before_exit line 15
2. def OAI.Problem367.IsingObservationFactor.canonicalClippedWeight line 31
3. lemma OAI.Problem367.IsingObservationFactor.canonicalClippedWeight_progressive line 36
4. lemma OAI.Problem367.IsingObservationFactor.canonicalClippedWeight_bound line 42
5. theorem OAI.Problem367.IsingObservationFactor.canonicalClippedWeight_continuous_ae line 47
6. theorem OAI.Problem367.IsingObservationFactor.canonicalClippedWeight_mul_covariance_before_exit line 56
7. theorem OAI.Problem367.IsingObservationFactor.canonicalClippedWeight_uniformSum_eq line 75