OAI/Probability/SpanningForest/PicardBounds.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336.DeterministicDecoder.picardBound line 12
  2. lemma OAI.Problem336.DeterministicDecoder.picardBound_nonneg line 15
  3. lemma OAI.Problem336.DeterministicDecoder.picardBound_le_exp_term line 20
  4. lemma OAI.Problem336.DeterministicDecoder.summable_picardBound line 35
  5. lemma OAI.Problem336.DeterministicDecoder.tendsto_picardBound_zero line 41
  6. theorem OAI.Problem336.DeterministicDecoder.exists_uniform_limit_of_summable_increments line 45
  7. theorem OAI.Problem336.DeterministicDecoder.exists_uniform_limit_of_picard_increments line 67
  8. theorem OAI.Problem336.DeterministicDecoder.unique_of_picard_approximation line 76
  9. theorem OAI.Problem336.DeterministicDecoder.uniform_drift_convergence line 95
  10. theorem OAI.Problem336.DeterministicDecoder.continuous_coordinate_of_uniform_limit line 118
  11. lemma OAI.Problem336.DeterministicDecoder.picardBound_mono_time line 127
  12. def OAI.Problem336.DeterministicDecoder.sequenceLimit line 132
  13. lemma OAI.Problem336.DeterministicDecoder.tendsto_sequenceLimit_of_picard_increments line 135
  14. theorem OAI.Problem336.DeterministicDecoder.compact_uniform_sequenceLimit line 145
  15. theorem OAI.Problem336.DeterministicDecoder.continuousOn_sequenceLimit line 170
  16. theorem OAI.Problem336.DeterministicDecoder.continuousOn_sequenceLimit_nonnegative line 182
  17. theorem OAI.Problem336.DeterministicDecoder.continuous_sequenceLimit_nnreal line 195
  18. theorem OAI.Problem336.DeterministicDecoder.integral_equation_at_of_uniform_limit line 203