OAI/Geometry/CylinderCovering/Ruled/Comparison.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RuledApproximation.comparisonOperator_apply line 9
  2. lemma OAI.RuledApproximation.comparisonOperator_eq_matrix line 15
  3. lemma OAI.RuledApproximation.comparisonOperator_trace line 19
  4. lemma OAI.RuledApproximation.comparisonOperator_det line 24
  5. lemma OAI.RuledApproximation.comparisonOperator_eigenvalues line 28
  6. lemma OAI.RuledApproximation.comparisonOperator_norm line 43
  7. lemma OAI.RuledApproximation.comparisonOperator_hyperbolic line 68
  8. theorem OAI.RuledApproximation.spectralNormComparison_proof line 76
  9. theorem OAI.RuledApproximation.physicalScalingInvariance_proof line 83
  10. lemma OAI.RuledApproximation.transverseScaling_fderiv line 93
  11. lemma OAI.RuledApproximation.rescaledComparisonOperator_apply line 105
  12. lemma OAI.RuledApproximation.rescaledComparisonOperator_norm line 111
  13. theorem OAI.RuledApproximation.physicalNormChange_proof line 130