OAI/Probability/FreeIsing/Gaussian/InwardCutConcentration.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.cutContinuationProduct_gaussianInwardConeFactor_le_cut line 16
2. theorem OAI.Problem367.average_gaussianInwardConeFactor_le_cut_average line 31
3. theorem OAI.Problem367.measure_gaussian_inward_path_average_ge_le line 72
4. theorem OAI.Problem367.measure_gaussian_inward_restricted_path_average_ge_le_double_exp line 111