OAI/Combinatorics/Progressions/Linear/FiniteKernelRestriction.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.finiteFiberAverage line 22
  2. theorem OAI.Erdos3.finiteFiberAverage_eq_of_map_eq line 25
  3. theorem OAI.Erdos3.finiteFiberAverage_integral_uniform line 39
  4. theorem OAI.Erdos3.finiteFiberAverage_continuous line 49
  5. theorem OAI.Erdos3.finiteFiberAverage_norm_le line 57
  6. theorem OAI.Erdos3.finiteFiberAverage_factor line 67
  7. theorem OAI.Erdos3.finiteFiberAverage_integral_of_invariant line 95
  8. def OAI.Erdos3.finiteKernelLiftLaw line 118
  9. theorem OAI.Erdos3.finiteKernelLiftLaw_integral line 122
  10. theorem OAI.Erdos3.finiteKernelLiftLaw_eq line 135
  11. theorem OAI.Erdos3.uniformPMF_map_equiv line 173
  12. theorem OAI.Erdos3.finiteKernelLiftLaw_relabel line 181
  13. theorem OAI.Erdos3.finiteKernelLiftLaw_basisResidues line 203
  14. theorem OAI.Erdos3.finiteKernelLift_density line 233
  15. theorem OAI.Erdos3.realDensityMeasure_indicator_one line 263
  16. theorem OAI.Erdos3.finiteKernelLift_restrict line 273