OAI/Analysis/DirectCrouzeix/Sharpness.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DirectCrouzeix.norm_entry_le_l2_opNorm line 17
  2. def OAI.DirectCrouzeix.sharpnessMatrix line 32
  3. def OAI.DirectCrouzeix.sharpnessCoefficients line 34
  4. theorem OAI.DirectCrouzeix.norm_le_one_of_mem_sharpnessRange line 36
  5. theorem OAI.DirectCrouzeix.sharpness_polynomialValue line 52
  6. theorem OAI.DirectCrouzeix.sharpness_tensorEvaluation line 56
  7. theorem OAI.DirectCrouzeix.sharpness_rangeMaximum_le_one line 61
  8. theorem OAI.DirectCrouzeix.sharpness_tensor_norm_ge_two line 68
  9. theorem OAI.DirectCrouzeix.uniform_sharpness line 75

    Distinct definitions of this name: ComparatorChallenges/DirectCrouzeix.lean:37 (same statement text; different proof or body). Qualify references as OAI.DirectCrouzeix.uniform_sharpness@path.