OAI/Combinatorics/Progressions/Geometry/ActualFixedSpatialRetainedPatchEndpoint.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_spatially_frozen_slice line 14
  2. def OAI.Erdos3.bufferedSpatialWeight line 75
  3. theorem OAI.Erdos3.bufferedSpatialWeight_eq_nearest line 80
  4. theorem OAI.Erdos3.bufferedSpatialWeight_mem_Icc line 89
  5. theorem OAI.Erdos3.bufferedSpatialWeight_lipschitz line 106
  6. theorem OAI.Erdos3.exists_spatially_frozen_buffered_slice line 128
  7. theorem OAI.Erdos3.ResidueBoxSlice.point_cast line 161
  8. theorem OAI.Erdos3.exists_spatially_localized_patch line 167
  9. def OAI.Erdos3.spatialPatchExtractionCost line 231
  10. theorem OAI.Erdos3.extraction_exp_two line 233
  11. theorem OAI.Erdos3.extraction_exp_four line 236
  12. theorem OAI.Erdos3.spatialPatchExtraction_radius line 245
  13. theorem OAI.Erdos3.spatialPatchExtraction_strict_budget line 249
  14. theorem OAI.Erdos3.spatialPatchExtraction_side_lower line 272
  15. theorem OAI.Erdos3.spatialPatchExtraction_large line 304
  16. theorem OAI.Erdos3.spatialPatchExtraction_gain_lower line 321
  17. theorem OAI.Erdos3.spatialPatchExtractionCost_le_power line 356
  18. theorem OAI.Erdos3.relativePatchSliceScore_reparamPatch line 389
  19. theorem OAI.Erdos3.relativePatchSliceConclusion_of_spatially_localized_patch line 401
  20. theorem OAI.Erdos3.relativePatchSliceConclusion_of_discounted_spatial_buffered_score line 437
  21. def OAI.Erdos3.spatialPatchExtractionMesh line 527
  22. theorem OAI.Erdos3.spatialPatchExtractionMesh_exp_le line 530
  23. theorem OAI.Erdos3.spatialPatchExtractionMesh_le_exp line 533
  24. theorem OAI.Erdos3.spatialPatchExtractionMesh_bounds line 538
  25. theorem OAI.Erdos3.spatialPatchExtractionMesh_pow_le line 558
  26. theorem OAI.Erdos3.spatialPatchExtraction_log_complexity_le_of_mesh line 567
  27. theorem OAI.Erdos3.spatialPatchExtraction_log_complexity_le line 614
  28. theorem OAI.Erdos3.exists_spatialPatchExtraction_parameters line 637
  29. theorem OAI.Erdos3.relativePatchSliceConclusion_of_budgeted_spatial_buffered_score line 683
  30. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.scaledRetainedRecoveredG line 788
  31. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastPath.relativePatchSliceConclusion_of_actual_retained_forecast_score line 793