OAI/Probability/JammingConcavity/VarianceTensorization.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Variance Tensorization.

  1. lemma OAI.MicroscopicJamming.memLp_two_swap line 47
  2. lemma OAI.MicroscopicJamming.integral_sq_ge_sq_integral line 51
  3. lemma OAI.MicroscopicJamming.memLp_two_integral_snd line 58
  4. lemma OAI.MicroscopicJamming.memLp_two_fiber_ae line 70
  5. lemma OAI.MicroscopicJamming.integrable_fiber_variance line 76
  6. lemma OAI.MicroscopicJamming.variance_prod_eq line 84
  7. lemma OAI.MicroscopicJamming.variance_integral_le line 99
  8. lemma OAI.MicroscopicJamming.integral_le_const_probability line 133
  9. def OAI.MicroscopicJamming.HasRowGrowth line 138
  10. lemma OAI.MicroscopicJamming.HasRowGrowth.memLp line 141
  11. lemma OAI.MicroscopicJamming.HasRowGrowth.cons line 153
  12. lemma OAI.MicroscopicJamming.measurePreserving_cons line 164
  13. theorem OAI.MicroscopicJamming.variance_pi_le_of_fiber line 174
  14. lemma OAI.MicroscopicJamming.gaussian_square_memLp_two line 238
  15. lemma OAI.MicroscopicJamming.coordinate_square_memLp_two line 244
  16. def OAI.MicroscopicJamming.rowNormSq line 251
  17. lemma OAI.MicroscopicJamming.rowNormSq_nonneg line 253
  18. lemma OAI.MicroscopicJamming.rowNormSq_memLp_two line 256
  19. lemma OAI.MicroscopicJamming.gaussian_potential_sq_integrable line 263
  20. def OAI.MicroscopicJamming.cavityMomentConstant line 272
  21. lemma OAI.MicroscopicJamming.cavityMoment_integrable line 274
  22. lemma OAI.MicroscopicJamming.cavityMomentConstant_nonneg line 278
  23. lemma OAI.MicroscopicJamming.gaussian_potential_sq_bound line 281
  24. lemma OAI.MicroscopicJamming.varianceMark_upper line 302
  25. lemma OAI.MicroscopicJamming.projected_potential_sq_bound line 307
  26. lemma OAI.MicroscopicJamming.potential_row_bound line 348
  27. lemma OAI.MicroscopicJamming.unitGround_rowGrowth line 355
  28. lemma OAI.MicroscopicJamming.unitEnergy_update line 371
  29. lemma OAI.MicroscopicJamming.unitGround_update_lower line 389
  30. lemma OAI.MicroscopicJamming.unitGround_cavity_upper line 396
  31. lemma OAI.MicroscopicJamming.memLp_unitGround_update line 406
  32. lemma OAI.MicroscopicJamming.variance_unitGround_fiber line 427
  33. theorem OAI.MicroscopicJamming.variance_unitGround_le_rows line 459
  34. lemma OAI.MicroscopicJamming.memLp_unitGround line 468
  35. lemma OAI.MicroscopicJamming.satProbability_le_variance_bound line 475
  36. def OAI.MicroscopicJamming.PositiveEnergyUnsatStatement line 515
  37. theorem OAI.MicroscopicJamming.positive_energy_implies_unsat line 523