OAI/NumberTheory/TwoPoint/Bounds/MatrixMomentNorm.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The unnormalized matrix moment controls the operator norm used in the spectral step.

  1. lemma OAI.TwoPointCorrelations.real_matrix_row_square line 16
  2. theorem OAI.TwoPointCorrelations.real_matrix_operator_norm_le line 27
  3. lemma OAI.TwoPointCorrelations.matrixOperator_mul line 44
  4. lemma OAI.TwoPointCorrelations.matrixOperator_one line 58
  5. lemma OAI.TwoPointCorrelations.matrixOperator_pow line 63
  6. def OAI.TwoPointCorrelations.complexifyMatrix line 69
  7. lemma OAI.TwoPointCorrelations.real_matrix_cast_mul line 72
  8. lemma OAI.TwoPointCorrelations.real_matrix_cast_pow line 78
  9. theorem OAI.TwoPointCorrelations.real_matrix_operator_power_norm_le line 89

    Source documentation

    The precise moment-to-operator inequality used by spectral transfer.

    theorem real_matrix_operator_power_norm_le (A : Matrix V V ℝ) (k : ℕ) :
    ‖matrixOperator (fun i j => (A i j : ℂ)) ^ k‖ ≤
      Real.sqrt (matrixFrobeniusSq (A ^ k)) := by
…

    Mentions: OAI.TwoPointCorrelations.matrixOperator, OAI.TwoPointCorrelations.matrixFrobeniusSq