OAI/Analysis/RotationWeights/Convolution.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CircleSampling.ConvolutionMasks line 85
  2. lemma OAI.CircleSampling.convolutionMasks_nonempty line 97
  3. def OAI.CircleSampling.convolutionMasks line 109
  4. lemma OAI.CircleSampling.model_ratio_bounds line 111
  5. lemma OAI.CircleSampling.model_ratio_masked line 124
  6. lemma OAI.CircleSampling.shifted_complement_squares line 143
  7. lemma OAI.CircleSampling.shifted_product_bound line 147
  8. lemma OAI.CircleSampling.modelTerm_enorm line 152
  9. lemma OAI.CircleSampling.modelRetained_cut line 161
  10. def OAI.CircleSampling.convolutionError line 189
  11. lemma OAI.CircleSampling.convolutionError_pos line 190
  12. lemma OAI.CircleSampling.convolutionError_eq line 191
  13. lemma OAI.CircleSampling.convolutionError_bound line 201
  14. lemma OAI.CircleSampling.integrated_retained_bound line 208
  15. lemma OAI.CircleSampling.projectionEvent_upper line 234
  16. theorem OAI.CircleSampling.model_no_strict_projection line 272