OAI/Probability/FreeIsing/Posterior/PlantedArrayCrossEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.stronglyMeasurable_latent_signalArrayFiltration line 13
2. theorem OAI.Problem367.planted_array_posterior_uniformSum_cross_energy line 24