OAI/Combinatorics/TriangleRemoval/Process/WitnessMu.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SharpTerminalLeave.witness_exp_series line 16
  2. theorem OAI.SharpTerminalLeave.three_segment_series line 21
  3. def OAI.SharpTerminalLeave.witnessMu line 30
  4. theorem OAI.SharpTerminalLeave.witnessMu_nonneg line 32
  5. theorem OAI.SharpTerminalLeave.witness_length_sum line 35
  6. theorem OAI.SharpTerminalLeave.witness_power_bound line 49