OAI/Combinatorics/Progressions/Estimates/AllocatedSlicedEndpointIdentity.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.jointSlicedProfileValue line 22
  2. def OAI.Erdos3.jointSlicedProfilePrincipal line 32
  3. theorem OAI.Erdos3.jointSlicedProfileValue_mul line 38
  4. theorem OAI.Erdos3.jointSlicedProfileValue_unit_scale line 55
  5. def OAI.Erdos3.jointSlicedProfileShift line 73
  6. def OAI.Erdos3.jointSlicedProfileTail line 77
  7. theorem OAI.Erdos3.jointSlicedProfileValue_split line 83
  8. theorem OAI.Erdos3.jointSlicedProfilePrincipal_unit_bounds line 101
  9. theorem OAI.Erdos3.jointSlicedProfilePrincipal_unit_mass line 120
  10. theorem OAI.Erdos3.jointSlicedProfileValue_unit_comparison line 135
  11. abbrev OAI.Erdos3.OneCubeActiveRow line 189
  12. abbrev OAI.Erdos3.OneCubeActiveEndpoint line 190
  13. def OAI.Erdos3.oneCubeProfileSubstitution line 194
  14. theorem OAI.Erdos3.oneCubeProfileSubstitution_principal line 203
  15. theorem OAI.Erdos3.oneCubeProfileSubstitution_degree line 210
  16. theorem OAI.Erdos3.oneCubeProfileSubstitution_mass line 223
  17. def OAI.Erdos3.oneCubeSlicedParameter line 242
  18. def OAI.Erdos3.oneCubeVertex line 250
  19. theorem OAI.Erdos3.oneCubeProfileSubstitution_eval line 252
  20. theorem OAI.Erdos3.booleanCoefficient_oneCube_reconstruct line 284
  21. def OAI.Erdos3.oneCubeJointJetEndpoints line 295
  22. theorem OAI.Erdos3.oneCubeJointJetEndpoints_measurable line 301
  23. def OAI.Erdos3.oneCubeProfileFrozenEndpoints line 307
  24. def OAI.Erdos3.oneCubeProfileEndpointNoise line 313
  25. theorem OAI.Erdos3.oneCubeProfileSubstitution_jet_identity line 319
  26. def OAI.Erdos3.oneCubeJetIndexEquiv line 353
  27. def OAI.Erdos3.oneCubeEndpointIndexEquiv line 363
  28. def OAI.Erdos3.oneCubeArrayPairEquiv line 369
  29. theorem OAI.Erdos3.oneCubeArrayPairEquiv_volume line 372
  30. def OAI.Erdos3.oneCubePairShear line 377
  31. def OAI.Erdos3.oneCubeJetEndpointEquiv line 385
  32. theorem OAI.Erdos3.oneCubeJetEndpointEquiv_volume line 392
  33. theorem OAI.Erdos3.oneCubeJetEndpointEquiv_apply line 403
  34. theorem OAI.Erdos3.oneCubeJointJetEndpoints_equiv line 409
  35. theorem OAI.Erdos3.oneCubeJointJetEndpoints_volume line 416
  36. def OAI.Erdos3.oneCubeSiteRestriction line 432
  37. theorem OAI.Erdos3.oneCubeSiteRestriction_lipschitz line 436
  38. theorem OAI.Erdos3.oneCubeSiteRestriction_complex_lipschitz line 445
  39. theorem OAI.Erdos3.oneCubeJointJetEndpoints_booleanSiteJets line 452
  40. theorem OAI.Erdos3.oneCubeJetEndpointEquiv_lipschitz line 473
  41. theorem OAI.Erdos3.oneCubeJet_norm_le line 493
  42. def OAI.Erdos3.oneCubeNormalizedSites line 523
  43. theorem OAI.Erdos3.oneCubeNormalizedSites_restriction line 530
  44. theorem OAI.Erdos3.oneCubeNormalizedSites_bound line 539
  45. def OAI.Erdos3.oneCubeBoundedJetEquiv line 568
  46. theorem OAI.Erdos3.boundedBooleanJetRows_oneCube line 574
  47. theorem OAI.Erdos3.realBoundedSiteReconstruction_oneCube line 580
  48. theorem OAI.Erdos3.oneCubeNormalizedSites_bounded_coordinates line 593
  49. theorem OAI.Erdos3.oneCube_endpoint_scale_product line 617
  50. theorem OAI.Erdos3.oneCube_bounded_scale_product line 622
  51. def OAI.Erdos3.VectorPolynomial.allocatedSlicedOneCubeEndpointMap line 656
  52. def OAI.Erdos3.VectorPolynomial.allocatedSlicedEndpointNoise line 663
  53. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedOneCubeEndpointMap_eq line 669