NonunitalJointPartition.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

An actual finite spectral partition in the original nonunital algebra. The augmentation-kernel calculation removes the origin cells; the mesh error is retained explicitly for the fixed-cut compression argument.

lemma OAI.WeakPureInfiniteness.norm_sum_productGridPlateau_subset_le line 20
lemma OAI.WeakPureInfiniteness.norm_of_joint_lift line 43
lemma OAI.WeakPureInfiniteness.norm_sub_sum_smul_joint_lifts line 48
lemma OAI.WeakPureInfiniteness.joint_lift_mul line 68
lemma OAI.WeakPureInfiniteness.joint_lift_sampledQuadraticError line 78
lemma OAI.WeakPureInfiniteness.norm_sum_of_joint_lifts line 93
lemma OAI.WeakPureInfiniteness.commute_of_joint_lifts line 109

theorem OAI.WeakPureInfiniteness.exists_nonunital_joint_partition line 121

Source documentation

Finite joint spectral localization for commuting positive elements. The sum-of-plateaux bound is independent of the mesh and of the number of cells.

theorem exists_nonunital_joint_partition (a : I → A) (ha : ∀ i, 0 ≤ a i)
    (hc : ∀ i j, Commute (a i) (a j)) (r : ℝ) (hr : 0 < r) :
    ∃ n : ℕ, ∃ f g : Fin n → A, ∃ t : I → Fin n → ℝ,
      (∀ j, 0 ≤ f j ∧ ‖f j‖ ≤ 1 ∧ 0 ≤ g j ∧ ‖g j‖ ≤ 1 ∧ f j * g j = g j) ∧
      ‖∑ j, f j‖ ≤ (5 : ℝ) ^ Fintype.card I ∧ ‖∑ j, g j‖ ≤ 1 ∧
      (∀ i j, 0 ≤ t i j) ∧
      (∀ i, ‖a i - ∑ j, (t i j : ℂ) • g j‖ ≤ r) ∧
      (∀ i j, Commute (a i) (f j) ∧ Commute (a i) (g j)) ∧
      (∀ j k, Commute (f j) (f k) ∧ Commute (f j) (g k) ∧ Commute (g j) (g k)) ∧
      (∀ i, ‖a i * a i - ∑ j, (((t i j) ^ 2 : ℝ) : ℂ) • g j‖ ≤ r ^ 2) ∧
      (∀ i, ‖∑ j, sampledQuadraticError (a i) (f j) (t i j)‖ ≤
        4 * r ^ 2 * (5 : ℝ) ^ Fintype.card I) ∧
…

Mentions: OAI.WeakPureInfiniteness.sampledQuadraticError