OAI/Topology/CoarseAssembly/CayleyNormControl.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A uniform Lipschitz estimate for the rational boundary unitary

  1. theorem OAI.CoarseAssembly.Analytic.cayleyDenominator_inverse_identity line 13
  2. theorem OAI.CoarseAssembly.Analytic.cayleyDenominator_inverse_norm_le line 23
  3. theorem OAI.CoarseAssembly.Analytic.cayleyDenominator_inverse_sub_norm_le line 32
  4. theorem OAI.CoarseAssembly.Analytic.cayleyUnitary_sub_norm_le line 52
  5. theorem OAI.CoarseAssembly.Analytic.rationalBoundaryUnitary_sub_norm_le line 64