OAI/Analysis/IrrationalRotation/Sampling/SamplingAsymptotics.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.SamplingAsymptotics.tendsto_pow_self_of_tendsto_zero line 12
  2. theorem OAI.Invariant233.SamplingAsymptotics.tendsto_logarithmic_diagonal line 24
  3. theorem OAI.Invariant233.SamplingAsymptotics.tendsto_source_diagonal line 47
  4. theorem OAI.Invariant233.SamplingAsymptotics.tendsto_dimension_mul_rpow line 53
  5. theorem OAI.Invariant233.SamplingAsymptotics.tendsto_one_add_pow line 63
  6. theorem OAI.Invariant233.SamplingAsymptotics.tendsto_one_sub_pow line 79
  7. theorem OAI.Invariant233.SamplingAsymptotics.tendsto_one_add_pow_pred line 92
  8. theorem OAI.Invariant233.SamplingAsymptotics.eventually_mem_unit_of_dimension_small line 103
  9. def OAI.Invariant233.SamplingAsymptotics.momentBase line 112
  10. def OAI.Invariant233.SamplingAsymptotics.kernelMass line 114
  11. def OAI.Invariant233.SamplingAsymptotics.productError line 116
  12. def OAI.Invariant233.SamplingAsymptotics.diagonalError line 120
  13. def OAI.Invariant233.SamplingAsymptotics.idealError line 124
  14. def OAI.Invariant233.SamplingAsymptotics.meanSquareBound line 126
  15. theorem OAI.Invariant233.SamplingAsymptotics.tendsto_momentBase_pow line 129
  16. theorem OAI.Invariant233.SamplingAsymptotics.tendsto_kernelMass_pow line 135
  17. theorem OAI.Invariant233.SamplingAsymptotics.tendsto_idealError line 145
  18. theorem OAI.Invariant233.SamplingAsymptotics.tendsto_productError line 153
  19. theorem OAI.Invariant233.SamplingAsymptotics.tendsto_meanSquareBound line 171