OAI/Combinatorics/Progressions/Geometry/CertifiedFullChartFrozenTerminal.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.allocatedParameterBox_coordinate_bound line 25
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedParameterBox_root_bound line 36
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedParameterBox_slice_cost line 43
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedParameterBox_side_eq line 69
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedFrozenParameterBox_mem line 73
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedFrozenParameterBox_bound line 87
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedParameterBox_physical_input line 121
  8. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_fullBox_normalized_approximation line 168
  9. theorem OAI.Erdos3.VectorPolynomial.integerSampledRealChart_freeze line 308
  10. theorem OAI.Erdos3.VectorPolynomial.integerSampledSpatial_freeze line 315
  11. theorem OAI.Erdos3.VectorPolynomial.integerSampledLowTags_freeze line 323
  12. def OAI.Erdos3.VectorPolynomial.allocatedFrozenIntegerFullChart line 344
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedFrozenIntegerFullChart_support line 353
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedFrozenIntegerFullChart_spatial line 368
  15. theorem OAI.Erdos3.VectorPolynomial.AllocatedCenteredFramedRecoveredSampleAt.integerFrozenFullChart_low_residual line 381
  16. theorem OAI.Erdos3.NilpotentLieFiltration.weightedAdaptedRealChartHom_integer_freeze line 433
  17. theorem OAI.Erdos3.NilpotentLieFiltration.weightedAdaptedRealChartHom_allocatedFrozenIntegerFullChart line 467
  18. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.allocatedFrozen_terminal_mem_fast line 524
  19. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.allocatedFrozen_terminal_mem_symbolPointwiseSubalgebra line 577