OAI/Combinatorics/Sensitivity/ProfileArithmetic.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The four raw recurrences imply the two normalized scalar recurrences.

  1. def OAI.Paper320.normalizedMax line 11
  2. theorem OAI.Paper320.normalizedMax_nonneg line 14
  3. theorem OAI.Paper320.le_normalizedMax_zero line 18
  4. theorem OAI.Paper320.le_normalizedMax_one line 22
  5. theorem OAI.Paper320.normalizedMax_le line 26
  6. theorem OAI.Paper320.raw_profiles_step line 32
  7. theorem OAI.Paper320.normalized_profiles_step line 62