OAI/Combinatorics/Progressions/FixedDensity/HypergraphBundleEnvelopeSelection.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.FixedDensity.HypergraphBundle.BaseWeightsIdempotent line 17
  2. def OAI.Erdos3.FixedDensity.HypergraphBundle.finsetMembershipEquivOfEq line 22
  3. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.finsetMembershipEquivOfEq_symm_val line 29
  4. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.cast_finsetPi_apply line 36
  5. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.projectionEquiv_apply_val line 51
  6. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.prod_comp_eq_prod_image_of_idempotent line 59
  7. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.doubledEdgeOfSource_eq_iff line 98
  8. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.pullbackBaseEdgeWeight_duplicateOutside_doubledEdge line 140
  9. def OAI.Erdos3.FixedDensity.HypergraphBundle.doubledBundleEdgeFactor line 257
  10. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.doubledBundleEdgeFactor_doubledEdgeOfSource line 265
  11. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.doubledBundleEdgeFactor_idempotent line 279
  12. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.doubledSourceProduct_pullback_eq_duplicateOutside_bundleProduct line 295
  13. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.doubledRemainderMoment_pullback_eq_duplicateOutside_bundleCount line 335
  14. def OAI.Erdos3.FixedDensity.HypergraphBundle.restrictEdgeTuple line 377
  15. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.restrictEdgeTuple_edgeTuple line 385
  16. def OAI.Erdos3.FixedDensity.HypergraphBundle.strictBoundaryLocalProduct line 392
  17. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.strictBoundaryLocalProduct_edgeTuple line 406
  18. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.strictBoundary_edges_subset_erase line 442
  19. def OAI.Erdos3.FixedDensity.HypergraphBundle.WeightsIdempotent line 452
  20. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.pullbackBaseEdgeWeight_weightsIdempotent line 459
  21. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.prod_mul_prod_eq_right_of_subset_of_idempotent line 469
  22. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.strictBoundaryLocalProduct_mul_edgeRemainder line 509
  23. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.edgeContribution_mul_strictBoundaryLocalProduct line 532
  24. def OAI.Erdos3.FixedDensity.HypergraphBundle.lowerExteriorMainProduct line 552
  25. def OAI.Erdos3.FixedDensity.HypergraphBundle.maximalRemainderMainProduct line 560
  26. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.card_image_projection line 567
  27. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.pow_card_edges_le_bundleMainProduct line 575
  28. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.bundleMainProduct_nonneg line 596
  29. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.bundleMainProduct_lowerOrder_eq_boundary_mul_exterior line 605
  30. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.boundary_mul_duplicateLower_main_eq_lowerOrder_sq line 647
  31. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.lowerOrder_mul_maximalRemainder_eq_erase_main line 661
  32. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.card_eq_selected_of_mem_maximalRemainder line 693
  33. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.card_maximalRemainder_le_erase line 706
  34. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.pow_card_maximalRemainder_le line 713
  35. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.pullbackBaseEdgeWeight_eq_of_projection_eq line 755
  36. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.doubledEdges_lowerOrder_subset line 837
  37. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.duplicateOutside_bundleProduct_le_lowerOrder line 855
  38. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.doubledRemainderMoment_pullback_le_lowerOrder line 899
  39. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.abs_edgeContribution_pullback_le_sqrt_boundary_mul_lowerOrder line 920
  40. structure OAI.Erdos3.FixedDensity.IsBundleCountingEnvelope line 1006
  41. def OAI.Erdos3.FixedDensity.bundleCountingStepIncrement line 1035
  42. theorem OAI.Erdos3.FixedDensity.IsBundleCountingEnvelope.add_stepIncrement_le line 1046
  43. theorem OAI.Erdos3.FixedDensity.IsBundleCountingEnvelope.lower_correction_nonneg line 1056
  44. def OAI.Erdos3.FixedDensity.bundleCommonStepIncrement line 1078
  45. def OAI.Erdos3.FixedDensity.bundleCommonNextRow line 1087
  46. def OAI.Erdos3.FixedDensity.bundleCommonEnvelopeError line 1094
  47. theorem OAI.Erdos3.FixedDensity.bundleCommonNextRow_zero line 1102
  48. theorem OAI.Erdos3.FixedDensity.bundleCommonNextRow_succ line 1108
  49. theorem OAI.Erdos3.FixedDensity.bundleCommonEnvelopeError_zero_order line 1116
  50. theorem OAI.Erdos3.FixedDensity.bundleCommonEnvelopeError_succ_order line 1122
  51. theorem OAI.Erdos3.FixedDensity.bundleCommonNextRow_nonneg line 1129
  52. theorem OAI.Erdos3.FixedDensity.bundleCommonEnvelopeError_nonneg line 1147
  53. theorem OAI.Erdos3.FixedDensity.bundleCommonStepIncrement_mono line 1160
  54. theorem OAI.Erdos3.FixedDensity.bundleCommonNextRow_mono line 1202
  55. theorem OAI.Erdos3.FixedDensity.bundleCommonEnvelopeError_monotone_card line 1221
  56. theorem OAI.Erdos3.FixedDensity.bundleCommonEnvelopeError_monotone_order line 1242
  57. theorem OAI.Erdos3.FixedDensity.bundleCommonEnvelopeError_isEnvelope line 1261
  58. theorem OAI.Erdos3.FixedDensity.bundleCommonNextRow_zero_parameter line 1297
  59. theorem OAI.Erdos3.FixedDensity.bundleCommonEnvelopeError_zero_parameter line 1310
  60. theorem OAI.Erdos3.FixedDensity.continuous_bundleCommonNextRow line 1324
  61. theorem OAI.Erdos3.FixedDensity.continuous_bundleCommonEnvelopeError_real line 1343
  62. theorem OAI.Erdos3.FixedDensity.tendsto_bundleCommonEnvelopeError_zero line 1367
  63. theorem OAI.Erdos3.FixedDensity.exists_bundleCommonEnvelopeError_lt line 1376
  64. theorem OAI.Erdos3.FixedDensity.exists_bundleCommonEnvelopeError_lt_half line 1430