OAI/Analysis/PureInfiniteness/UltrapowerMatrixCut.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The fixed-cut diagonalization in the norm ultrapower, for arbitrary ultrapower entries. Positive representatives and a uniform finite coefficient bound are the only lifting ingredients.

  1. def OAI.WeakPureInfiniteness.boundedCoordinate line 24
  2. lemma OAI.WeakPureInfiniteness.boundedCoordinate_apply line 32
  3. lemma OAI.WeakPureInfiniteness.positive_bounded_representative line 36
  4. theorem OAI.WeakPureInfiniteness.boundedFamilies_cut_diagonalization line 55
  5. theorem OAI.WeakPureInfiniteness.ultrapower_matrix_cut_diagonalization line 117

    Source documentation

    KR02's exact cut diagonalization for a finite family in the norm ultrapower. The matrix entries themselves need not be constant sequences.

    theorem ultrapower_matrix_cut_diagonalization (hP : MainGap.PropertyP A)
    (U : Ultrafilter ℕ) [Fact ((U : Filter ℕ) ≤ atTop)]
    (M₀ : ℝ) (δ : ℝ≥0) (hδ : 0 < δ) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ n : ℕ,
      ∀ M : Fin n → Fin n → NormUltra.QuotientAlgebra (fun _ : ℕ => A) U,
      (∀ i, 0 ≤ M i i) → (∀ i, ‖M i i‖ ≤ M₀) →
      ∃ d : Fin n → NormUltra.QuotientAlgebra (fun _ : ℕ => A) U,
      (∀ i, ‖d i‖ ≤ C) ∧
      (∀ i, star (d i) * M i i * d i = MainGap.cut (M i i) δ) ∧
      ∀ i j, i ≠ j → star (d i) * M i j * d j = 0 := by
…

    Mentions: OAI.MainGap.PropertyP, OAI.NormUltra.QuotientAlgebra, OAI.MainGap.cut