OAI/Analysis/LipschitzHilbert/Estimates/ExponentialVariation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Variation of exponential weights from variation of their logarithms.

  1. theorem OAI.LipschitzHilbert.norm_exp_sub_le_of_re_le line 15
  2. theorem OAI.LipschitzHilbert.exponential_sequence_variation line 33
  3. theorem OAI.LipschitzHilbert.logarithm_increment_bound line 51
  4. theorem OAI.LipschitzHilbert.exponential_hierarchy_variation line 61