OAI/Analysis/Crouzeix/TensorDensity.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Tensor Density.

  1. theorem OAI.CrouzeixHilbert.tensorOperator_one line 31
  2. theorem OAI.CrouzeixHilbert.tensorOperator_mul line 43
  3. theorem OAI.CrouzeixHilbert.tensorOperator_star line 55
  4. def OAI.CrouzeixHilbert.amplifiedRoot line 82
  5. def OAI.CrouzeixHilbert.coefficientField line 88
  6. theorem OAI.CrouzeixHilbert.amplifiedRoot_star_mul line 94
  7. theorem OAI.CrouzeixHilbert.amplifiedRoot_mass line 102
  8. theorem OAI.CrouzeixHilbert.amplifiedRoot_sandwich line 111
  9. theorem OAI.CrouzeixHilbert.norm_integral_tensor_density_le line 119
  10. theorem OAI.CrouzeixHilbert.Disk.integral_matrixPolynomial line 147
  11. theorem OAI.CrouzeixHilbert.Disk.polynomial_bound_spectralRadius_lt_one line 173
  12. theorem OAI.CrouzeixHilbert.Disk.continuous_polynomialEval line 189
  13. theorem OAI.CrouzeixHilbert.Disk.radial_tendsto_polynomialEval line 195
  14. lemma OAI.CrouzeixHilbert.Disk.spectralRadius_lt_one_of_norm_lt_one line 207
  15. theorem OAI.CrouzeixHilbert.Disk.polynomial_bound_nontrivial line 212
  16. theorem OAI.CrouzeixHilbert.Disk.polynomial_bound line 225