OAI/Combinatorics/Progressions/Sampling/ForecastLawRecoveredRationalCardinalityCap.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.forecastFrozenIntegerMixedValue line 20
  2. theorem OAI.Erdos3.VectorPolynomial.taggedAmbient_lipschitz line 26
  3. theorem OAI.Erdos3.VectorPolynomial.forecastFrozenIntegerMixedValue_lipschitz line 34
  4. theorem OAI.Erdos3.VectorPolynomial.forecastFrozenIntegerActiveCoordinates_lipschitz line 57
  5. def OAI.Erdos3.VectorPolynomial.forecastRecoveredIntegerLabels line 119
  6. def OAI.Erdos3.VectorPolynomial.forecastLawRecoveredRationalFactor line 124
  7. def OAI.Erdos3.VectorPolynomial.forecastLawRecoveredKernel line 135
  8. theorem OAI.Erdos3.VectorPolynomial.forecastLawRecoveredRationalFactor_nonneg line 150
  9. theorem OAI.Erdos3.VectorPolynomial.forecastLawRecoveredKernel_mem_Icc line 154
  10. theorem OAI.Erdos3.VectorPolynomial.forecastLawRecoveredKernel_lift_lipschitz line 167
  11. theorem OAI.Erdos3.VectorPolynomial.forecastLawRecoveredKernel_spatial_lipschitz line 192
  12. theorem OAI.Erdos3.VectorPolynomial.forecastLawRecoveredRationalFactor_eq_of_labels line 271
  13. theorem OAI.Erdos3.VectorPolynomial.forecastLawRecoveredKernel_eq_of_labels line 289
  14. theorem OAI.Erdos3.VectorPolynomial.forecastLawRecoveredKernel_recovered_invariant line 303
  15. theorem OAI.Erdos3.VectorPolynomial.forecastLawDensityPhysicalDeckSource_eq_recoveredKernel line 372
  16. theorem OAI.Erdos3.VectorPolynomial.forecastRecoveredPhysicalDeck line 398
  17. theorem OAI.Erdos3.VectorPolynomial.forecastRecoveredPhysicalPoint line 434
  18. theorem OAI.Erdos3.VectorPolynomial.forecastLawDensityPhysicalTarget_eq_recoveredKernel line 459
  19. theorem OAI.Erdos3.VectorPolynomial.forecastLawRecoveredRationalFactor_le_of_decay line 535
  20. theorem OAI.Erdos3.VectorPolynomial.forecastLawRecoveredRationalFactor_abs_le_of_decay line 556
  21. theorem OAI.Erdos3.VectorPolynomial.forecastLawRecoveredRationalFactor_le_exp_of_grid_modulus line 626