OAI/Analysis/RotationWeights/LaurentCoefficients.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ContinuousCircleWeight.fiber_squares line 83
  2. lemma OAI.ContinuousCircleWeight.fiber_squares_le line 90
  3. lemma OAI.ContinuousCircleWeight.fiber_product_le line 94
  4. lemma OAI.ContinuousCircleWeight.projection_vector_norm line 104
  5. def OAI.ContinuousCircleWeight.laurentArray line 114
  6. def OAI.ContinuousCircleWeight.retainedIndices line 115
  7. lemma OAI.ContinuousCircleWeight.mem_retainedIndices line 116
  8. lemma OAI.ContinuousCircleWeight.laurent_coeff line 119
  9. lemma OAI.ContinuousCircleWeight.lowProduct_convolution line 122
  10. def OAI.CircleSampling.modelColumn line 166
  11. def OAI.CircleSampling.modelComplement line 167
  12. def OAI.CircleSampling.modelDiagonal line 168
  13. lemma OAI.CircleSampling.modelColumn_norm line 169
  14. lemma OAI.CircleSampling.modelComplement_norm line 170
  15. lemma OAI.CircleSampling.modelColumn_measurable line 171
  16. lemma OAI.CircleSampling.modelComplement_measurable line 172
  17. lemma OAI.CircleSampling.modelColumn_coordinate line 174
  18. lemma OAI.CircleSampling.modelComplement_coordinate line 176
  19. lemma OAI.CircleSampling.modelDiagonal_measurable line 178
  20. def OAI.CircleSampling.modelTerm line 180
  21. def OAI.CircleSampling.modelRetained line 182
  22. lemma OAI.CircleSampling.modelTerm_measurable line 184
  23. lemma OAI.CircleSampling.modelRetained_measurable line 190
  24. lemma OAI.CircleSampling.regular_model_order line 193
  25. lemma OAI.CircleSampling.model_pair_convolution line 196
  26. lemma OAI.CircleSampling.model_convolution_ae line 218
  27. def OAI.CircleSampling.modelCoefficientPair line 227
  28. lemma OAI.CircleSampling.modelCoefficient_identity line 230
  29. lemma OAI.CircleSampling.modelColumn_coordinate_bound line 243
  30. lemma OAI.CircleSampling.modelComplement_coordinate_bound line 245
  31. lemma OAI.CircleSampling.modelComplement_zero_re line 247
  32. lemma OAI.CircleSampling.modelCoefficient_bounds line 252
  33. lemma OAI.CircleSampling.modelCoefficient_centers line 272
  34. lemma OAI.CircleSampling.model_coefficient_lower line 284
  35. lemma OAI.CircleSampling.all_masks line 299
  36. def OAI.CircleSampling.longIndex line 310
  37. lemma OAI.CircleSampling.longIndex_long line 311