OAI/Combinatorics/Progressions/Polynomial/PolynomialPatchShearOrbitConverse.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.realPolynomialMass_weightedComponent_le line 15
  2. theorem OAI.Erdos3.realPolynomialMass_zeroParameterEval_le line 29
  3. theorem OAI.Erdos3.PolynomialSlots.topPart_specializeCenter_mass_le line 45
  4. theorem OAI.Erdos3.PolynomialSlots.center_mass_le_of_normalized line 56
  5. def OAI.Erdos3.PolynomialSlots.shearTransformedSlots line 91
  6. theorem OAI.Erdos3.PolynomialSlots.shearTransformedSlots_residual line 109
  7. theorem OAI.Erdos3.PolynomialPatch.shearSummand_eq_residual line 128
  8. theorem OAI.Erdos3.PolynomialPatch.shearSummand_unique line 136
  9. theorem OAI.Erdos3.PolynomialPatch.shearOrbitSum_eq_patchValue line 146
  10. theorem OAI.Erdos3.PolynomialPatch.shearObservable_mem_Icc line 154
  11. theorem OAI.Erdos3.PolynomialPatch.abs_shearObservable_le_one line 163
  12. def OAI.Erdos3.symbolicShearPrefixSubstitution line 181
  13. theorem OAI.Erdos3.symbolicShearPrefixSubstitution_degree line 186
  14. def OAI.Erdos3.PolynomialPatch.symbolicShearFullCenter line 209
  15. theorem OAI.Erdos3.PolynomialPatch.symbolicShearFullCenter_degree line 218
  16. def OAI.Erdos3.PolynomialPatch.symbolicShearForm line 229
  17. def OAI.Erdos3.PolynomialPatch.symbolicShearPatch line 235
  18. theorem OAI.Erdos3.PolynomialPatch.symbolicShearFullCenter_eval line 248
  19. theorem OAI.Erdos3.PolynomialPatch.symbolicShearForm_slots line 264
  20. theorem OAI.Erdos3.PolynomialPatch.symbolicShearPatch_value line 292
  21. theorem OAI.Erdos3.PolynomialPatch.symbolicShearPatch_value_eq_observable line 302
  22. theorem OAI.Erdos3.PolynomialSlots.topResidualEquiv_X_mass line 329
  23. theorem OAI.Erdos3.PolynomialSlots.topResidualEquiv_inverse_mass line 337
  24. theorem OAI.Erdos3.PolynomialSlots.topResidualEquiv_inverse_X_mass line 347
  25. theorem OAI.Erdos3.PolynomialSlots.topResidualEquiv_inverse_eval_bound line 355
  26. theorem OAI.Erdos3.PolynomialSlots.topResidualPoint_preimage_bound line 363
  27. theorem OAI.Erdos3.PolynomialPatch.shearKernel_support_bound line 382
  28. theorem OAI.Erdos3.PolynomialPatch.normalized_shearKernel_support_bound line 391
  29. theorem OAI.Erdos3.symbolicShearPrefixSubstitution_slot_degree line 411
  30. def OAI.Erdos3.PolynomialPatch.symbolicShearTopCenter line 433
  31. theorem OAI.Erdos3.PolynomialPatch.symbolicShearTopCenter_eq line 436
  32. theorem OAI.Erdos3.PolynomialPatch.symbolicShearTopCenter_homogeneous line 445
  33. theorem OAI.Erdos3.PolynomialPatch.symbolicShearPrefix_topResidual line 456
  34. theorem OAI.Erdos3.PolynomialPatch.symbolicShearForm_center_sub_top_lower line 480
  35. theorem OAI.Erdos3.PolynomialPatch.symbolicShearForm_topPart_center line 507
  36. theorem OAI.Erdos3.PolynomialPatch.symbolicShearForm_topPart_specializeCenter line 515
  37. theorem OAI.Erdos3.PolynomialPatch.symbolicShearForm_topResidualEquiv line 524
  38. theorem OAI.Erdos3.PolynomialPatch.symbolicShearForm_specialized_residualHom line 539
  39. theorem OAI.Erdos3.PolynomialPatch.symbolicShearForm_loweringAt line 556
  40. theorem OAI.Erdos3.PolynomialPatch.symbolicShearForm_shearGroupLift line 570
  41. theorem OAI.Erdos3.PolynomialSlots.shearPatchValue_dist line 592
  42. def OAI.Erdos3.polynomialShearOrbitSymbolicHom line 633
  43. theorem OAI.Erdos3.polynomialShearOrbitSymbolicHom_degree line 639
  44. theorem OAI.Erdos3.polynomialShearOrbitSymbolicHom_specialization line 648
  45. theorem OAI.Erdos3.polynomialShearOrbitSymbolicHom_lower line 657
  46. def OAI.Erdos3.PolynomialPatch.ofShearOrbit line 668
  47. theorem OAI.Erdos3.PolynomialPatch.ofShearOrbit_weight line 675
  48. theorem OAI.Erdos3.PolynomialPatch.ofShearOrbit_kernel line 679
  49. theorem OAI.Erdos3.PolynomialPatch.ofShearOrbit_value_real line 683
  50. theorem OAI.Erdos3.PolynomialPatch.ofShearOrbit_value_integer line 701
  51. theorem OAI.Erdos3.PolynomialPatch.ofShearOrbit_shearGroupLift_real line 709
  52. theorem OAI.Erdos3.PolynomialPatch.ofShearOrbit_shearGroupLift_integer line 728
  53. theorem OAI.Erdos3.PolynomialPatch.exists_patch_of_shear_orbit line 736