OAI/Analysis/DirectCrouzeix/KernelContraction.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DirectCrouzeix.Faber.weighted_integral_norm_sq_le line 19
  2. theorem OAI.DirectCrouzeix.Faber.continuous_integrable_compact line 50
  3. theorem OAI.DirectCrouzeix.Faber.continuous_integral_compact line 56
  4. theorem OAI.DirectCrouzeix.Faber.markov_kernel_contraction line 65
  5. def OAI.DirectCrouzeix.Faber.positiveSeries line 101
  6. theorem OAI.DirectCrouzeix.Faber.continuous_positiveSeries line 104
  7. theorem OAI.DirectCrouzeix.Faber.fourierCoeff_finite_smul line 109
  8. theorem OAI.DirectCrouzeix.Faber.fourierCoeff_positiveSeries line 119
  9. theorem OAI.DirectCrouzeix.Faber.integral_inner_positiveSeries line 133
  10. theorem OAI.DirectCrouzeix.Faber.energy_positiveSeries line 151
  11. theorem OAI.DirectCrouzeix.Faber.energy_orthogonal_positiveSeries line 162