OAI/Combinatorics/Progressions/Estimates/CoveredInducedCorrelationFamily.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_markedShift_evaluation_model_with_budget line 24
  2. theorem OAI.Erdos3.exists_compatible_marked_evaluation_model line 110
  3. theorem OAI.Erdos3.exists_normalized_marked_model line 222
  4. theorem OAI.Erdos3.exists_induced_marked_observable line 315
  5. theorem OAI.Erdos3.exists_induced_marked_model line 374
  6. theorem OAI.Erdos3.exists_native_induced_marked_model line 464
  7. abbrev OAI.Erdos3.QuadraticMarked.Seed line 576
  8. def OAI.Erdos3.QuadraticMarked.filtration line 578
  9. def OAI.Erdos3.QuadraticMarked.generators line 581
  10. def OAI.Erdos3.QuadraticMarked.weights line 583
  11. def OAI.Erdos3.QuadraticMarked.marked line 585
  12. theorem OAI.Erdos3.QuadraticMarked.weight_pos line 587
  13. theorem OAI.Erdos3.QuadraticMarked.generator_mem line 591
  14. theorem OAI.Erdos3.QuadraticMarked.second_marked_span line 596
  15. abbrev OAI.Erdos3.QuadraticMarked.Algebra line 601
  16. def OAI.Erdos3.QuadraticMarked.multidegree line 603
  17. def OAI.Erdos3.QuadraticMarked.phase line 607
  18. def OAI.Erdos3.QuadraticMarked.evaluation line 609
  19. def OAI.Erdos3.QuadraticMarked.localCharacter line 612
  20. def OAI.Erdos3.QuadraticMarked.Model line 619
  21. theorem OAI.Erdos3.QuadraticMarked.Model.mono line 637
  22. theorem OAI.Erdos3.QuadraticMarked.filtration_layers line 649
  23. theorem OAI.Erdos3.QuadraticMarked.structure_height line 654
  24. theorem OAI.Erdos3.QuadraticMarked.generator_height line 658
  25. theorem OAI.Erdos3.QuadraticMarked.exists_model_from_seed line 663
  26. theorem OAI.Erdos3.QuadraticMarked.exists_model line 701
  27. def OAI.Erdos3.NativeRankRelation.CommonData.HasCommonInducedCorrelationFamily line 755
  28. theorem OAI.Erdos3.NativeRankRelation.CommonData.hasCommonInducedCorrelationFamily_of_model line 814
  29. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_common_induced_correlation_family line 904
  30. theorem OAI.Erdos3.NativeRankRelation.CommonData.HasCommonInducedCorrelationFamily.mono line 981
  31. def OAI.Erdos3.NativeRankRelation.CommonData.HasCoveredInducedCorrelationFamily line 1063
  32. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_covered_induced_correlation_family line 1093