OAI/Geometry/BallPacking/Models/CubicPhysicalLocality.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.globalHorizontalCoupling_congr_germs line 16
  2. theorem OAI.PackingSufficiencySupport.CubicModel.physicalParameter_fiber_lower_near line 32
  3. theorem OAI.PackingSufficiencySupport.CubicModel.physicalPrimitive_representative_fiber_germ line 44
  4. theorem OAI.PackingSufficiencySupport.CubicModel.physicalCoupling_representative_near line 63
  5. theorem OAI.PackingSufficiencySupport.exists_positive_common_denominator line 86
  6. def OAI.PackingSufficiencySupport.truncatedSimplex line 106
  7. theorem OAI.PackingSufficiencySupport.truncatedSimplex_isClosed line 109
  8. theorem OAI.PackingSufficiencySupport.truncatedSimplex_isCompact line 118
  9. theorem OAI.PackingSufficiencySupport.truncatedSimplex_fubini line 127
  10. theorem OAI.PackingSufficiencySupport.integral_truncated_simplex_power line 153
  11. theorem OAI.PackingSufficiencySupport.volumeReal_truncatedSimplex line 171
  12. theorem OAI.PackingSufficiencySupport.integral_truncated_tent line 176
  13. theorem OAI.PackingSufficiencySupport.integral_truncated_cap line 181
  14. theorem OAI.PackingSufficiencySupport.integral_truncated_affine line 203
  15. def OAI.PackingSufficiencySupport.sixModelMean line 219
  16. theorem OAI.PackingSufficiencySupport.integral_six_model line 222
  17. theorem OAI.PackingSufficiencySupport.continuous_sixModelMean line 237
  18. theorem OAI.PackingSufficiencySupport.sixModelMean_limit_value line 242
  19. def OAI.PackingSufficiencySupport.momentHeadTail line 247
  20. theorem OAI.PackingSufficiencySupport.momentHeadTail_apply line 250
  21. theorem OAI.PackingSufficiencySupport.momentHeadTail_symm_apply line 254
  22. theorem OAI.PackingSufficiencySupport.continuous_momentHeadTail line 260
  23. theorem OAI.PackingSufficiencySupport.continuous_momentHeadTail_symm line 264
  24. theorem OAI.PackingSufficiencySupport.isCompact_preimage_momentHeadTail line 271
  25. theorem OAI.PackingSufficiencySupport.integral_momentHeadTail line 283
  26. def OAI.PackingSufficiencySupport.sixModelBounds line 295
  27. theorem OAI.PackingSufficiencySupport.sixModelBounds_nonneg line 297
  28. theorem OAI.PackingSufficiencySupport.sixModelBounds_le_one line 301
  29. theorem OAI.PackingSufficiencySupport.sixModelRegion_eq line 305
  30. theorem OAI.PackingSufficiencySupport.sixModelRegion_isCompact line 320
  31. theorem OAI.PackingSufficiencySupport.sixModelRegion_contains_cap line 325
  32. def OAI.PackingSufficiencySupport.sixModelDensity line 337
  33. def OAI.PackingSufficiencySupport.sixModelGap line 340
  34. theorem OAI.PackingSufficiencySupport.continuous_sixModelGap line 343
  35. theorem OAI.PackingSufficiencySupport.sixModelGap_eq_cappedAffine line 348
  36. theorem OAI.PackingSufficiencySupport.integral_sixModelDensity line 356
  37. theorem OAI.PackingSufficiencySupport.integral_sixModelGap line 371
  38. theorem OAI.PackingSufficiencySupport.sixModelDensity_lower line 389
  39. theorem OAI.PackingSufficiencySupport.CubicModel.physicalArea_eq_sixModelDensity line 406
  40. theorem OAI.PackingSufficiencySupport.CubicModel.exists_six_cubic_weights line 421
  41. theorem OAI.PackingSufficiencySupport.CubicModel.physicalParameter_maps_six_region line 464
  42. theorem OAI.PackingSufficiencySupport.CubicModel.exists_six_cubic_inner_weights line 483
  43. theorem OAI.PackingSufficiencySupport.CubicModel.exists_six_cubic_inner_weights_large line 531
  44. theorem OAI.PackingSufficiencySupport.rational_truncation_pair line 568
  45. theorem OAI.PackingSufficiencySupport.cap_into_scaled_region line 585
  46. theorem OAI.PackingSufficiencySupport.sum_caps_zero_outside line 605