OAI/Combinatorics/SumProduct/Alignment/RoughSampling02.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RoughKernelFactorization.residueSigma line 34
  2. theorem OAI.RoughKernelFactorization.finite_residue_kernel_reduction line 40
  3. def OAI.RoughSamplingWeights.rescaledEndpoint line 123
  4. def OAI.RoughSamplingWeights.integerAffine line 126
  5. lemma OAI.RoughSamplingWeights.rescaled_box line 129
  6. def OAI.RoughSamplingWeights.physicalResidueBox line 142
  7. lemma OAI.RoughSamplingWeights.physical_residue_reparametrization line 145
  8. lemma OAI.RoughSamplingWeights.mean_image line 161
  9. theorem OAI.RoughSamplingWeights.residue_mean line 170
  10. theorem OAI.RoughSamplingWeights.residual_congruences line 181
  11. theorem OAI.RoughSamplingWeights.residual_mean line 189
  12. theorem OAI.RoughSamplingWeights.rescaled_geometry line 206
  13. lemma OAI.RealPolynomialDegree.affine_substitution_totalDegree line 247
  14. theorem OAI.RealPolynomialDegree.affine_comp line 271