OAI/Probability/FreeIsing/Stochastic/BinaryFusionIntegral.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.ae_binaryFusion_bounds line 11
  2. theorem OAI.Problem367.integrable_binaryFusion_integrand line 21

    Distinct definitions of this name: OAI/Probability/FreeIsing/Gaussian/BinaryFusionInformation.lean:35 (different declaration text). Qualify references as OAI.Problem367.integrable_binaryFusion_integrand@path.

  3. theorem OAI.Problem367.integrable_binaryFusionLoss line 34
  4. theorem OAI.Problem367.integral_binaryFusion_symmetric_square line 49
  5. theorem OAI.Problem367.integral_binaryFusionLoss_nonneg line 103
  6. theorem OAI.Problem367.integral_binaryFusion_le_sum_sq line 111
  7. theorem OAI.Problem367.integrable_sq_of_ae_abs_lt_one line 120
  8. theorem OAI.Problem367.integral_binaryFusionLoss_lower_bound line 128
  9. theorem OAI.Problem367.integral_binaryFusion_le_sum_sq_sub_loss line 153