OAI/Analysis/NuclearUltrapower/SOSGap.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.NuclearUltrapower.SOSEnergy.energy line 15
2. theorem OAI.NuclearUltrapower.SOSEnergy.energy_nonneg line 18
3. theorem OAI.NuclearUltrapower.SOSEnergy.word_norm_bound line 22

   Source documentation

   Telescoping a word uses only the unitary relations and the specified generators.

   theorem word_norm_bound (ρ : Γ →* (H ≃ₗᵢ[ℂ] H)) (x : H) (r : ℝ)
       (w : List Γ) (hw : ∀ s ∈ w, ‖ρ s x - x‖ ≤ r) :
       ‖ρ w.prod x - x‖ ≤ w.length * r := by
   …

4. theorem OAI.NuclearUltrapower.SOSEnergy.word_sq_bound line 45

   Source documentation

   A length-at-most-four word has energy bounded by sixteen times the generator energy.

   theorem word_sq_bound (S : Finset Γ) (ρ : Γ →* (H ≃ₗᵢ[ℂ] H)) (x : H)
       (w : List Γ) (hw : ∀ s ∈ w, s ∈ S) (hlen : w.length ≤ 4) :
       ‖ρ w.prod x - x‖ ^ 2 ≤ 16 * energy S ρ x := by
   …

   Mentions: OAI.NuclearUltrapower.SOSEnergy.energy

5. theorem OAI.NuclearUltrapower.SOSEnergy.real_inner_unitary line 60

   Source documentation

   The exact real quadratic form of a unitary displacement.

   theorem real_inner_unitary (ρ : Γ →* (H ≃ₗᵢ[ℂ] H)) (g : Γ) (x : H) :
       (inner ℂ x (ρ g x)).re = ‖x‖ ^ 2 - ‖ρ g x - x‖ ^ 2 / 2 := by
   …

6. def OAI.NuclearUltrapower.SOSEnergy.reInnerAdd line 67
7. def OAI.NuclearUltrapower.SOSEnergy.polyVector line 70
8. theorem OAI.NuclearUltrapower.SOSEnergy.polyVector_real_inner line 73
9. theorem OAI.NuclearUltrapower.SOSEnergy.weighted_displacement_le line 92

   Source documentation

   An integer coefficient may have either sign; absolute coefficients suffice.

   theorem weighted_displacement_le (ρ : Γ →* (H ≃ₗᵢ[ℂ] H)) (x : H)
       (p : List (Γ × ℤ)) (M : ℝ)
       (hb : ∀ a ∈ p, ‖ρ a.1 x - x‖ ^ 2 ≤ M) :
       (p.map (fun a => (a.2 : ℝ) * ‖ρ a.1 x - x‖ ^ 2)).sum ≤
         ((p.map (fun a => |a.2|)).sum : ℤ) * M := by
   …

10. theorem OAI.NuclearUltrapower.SOSEnergy.residual_lower line 109

    Source documentation

    Exact augmentation zero converts a short supported residual into an energy error. The constant eight here combines the squared word bound 16 with the factor 1/2.

    theorem residual_lower (S : Finset Γ) (ρ : Γ →* (H ≃ₗᵢ[ℂ] H)) (x : H)
        (p : List (Γ × ℤ)) (haug : (p.map Prod.snd).sum = 0)
        (hsupp : ∀ a ∈ p, ∃ w : List Γ, w.prod = a.1 ∧ w.length ≤ 4 ∧ ∀ s ∈ w, s ∈ S) :
        -(8 * ((p.map (fun a => |a.2|)).sum : ℤ) * energy S ρ x) ≤
          (inner ℂ x (polyVector ρ x p)).re := by
    …

    Mentions: OAI.NuclearUltrapower.SOSEnergy.energy, OAI.NuclearUltrapower.SOSEnergy.polyVector

11. theorem OAI.NuclearUltrapower.positive_sq_gap line 131

    Source documentation

    A sums-of-squares inequality for a positive operator produces a true gap on the orthogonal complement of its kernel; no finite-dimensional hypothesis.

    theorem positive_sq_gap (T : H →L[ℂ] H) (hT : 0 ≤ T) (κ : ℝ)
        (hgap : κ • T ≤ T*T) (x : H) (hx : x ∈ T.kerᗮ) :
        κ * ‖x‖ ^ 2 ≤ (inner ℂ x (T x)).re := by
    …

12. def OAI.NuclearUltrapower.SOSEnergy.polyOperator line 186
13. theorem OAI.NuclearUltrapower.SOSEnergy.polyOperator_apply line 190
14. theorem OAI.NuclearUltrapower.SOSEnergy.certificate_sq_gap line 200

    Source documentation

    The rational certificate's defect absorption, with its exact denominator and certified l1 size. The support/augmentation premises will be discharged by the matrix-labelled reflection certificate, never assumed of the main group.

    theorem certificate_sq_gap (S : Finset Γ) (ρ : Γ →* (H ≃ₗᵢ[ℂ] H))
        (D Q : H →L[ℂ] H) (p : List (Γ × ℤ))
        (hD : 0 ≤ D) (hQ : 0 ≤ Q)
        (henergy : ∀ x, (inner ℂ x (D x)).re = energy S ρ x / 2)
        (haug : (p.map Prod.snd).sum = 0)
        (hl1 : (p.map (fun a => |a.2|)).sum = 29562852800)
        (hsupp : ∀ a ∈ p, ∃ w : List Γ, w.prod = a.1 ∧ w.length ≤ 4 ∧ ∀ s ∈ w, s ∈ S)
        (hcert : (10000000000000 : ℝ) • (D*D) - (1000000000000 : ℝ) • D =
          Q + polyOperator ρ p) : (1 / 20 : ℝ) • D ≤ D*D := by
    …

    Mentions: OAI.NuclearUltrapower.SOSEnergy.energy, OAI.NuclearUltrapower.SOSEnergy.polyOperator

15. theorem OAI.NuclearUltrapower.SOS.ElementarySpectral.genList_nodup line 249
16. theorem OAI.NuclearUltrapower.SOS.ElementarySpectral.eGenSet_card line 259
17. def OAI.NuclearUltrapower.SOS.ElementarySpectral.value line 266
18. theorem OAI.NuclearUltrapower.SOS.ElementarySpectral.value_one line 268
19. theorem OAI.NuclearUltrapower.SOS.ElementarySpectral.value_mul line 271
20. theorem OAI.NuclearUltrapower.SOS.ElementarySpectral.value_inv line 276
21. theorem OAI.NuclearUltrapower.SOS.ElementarySpectral.delta_value line 281
22. theorem OAI.NuclearUltrapower.SOS.ElementarySpectral.sum_gen_star line 289
23. theorem OAI.NuclearUltrapower.SOS.ElementarySpectral.laplacian_eq_delta line 298
24. theorem OAI.NuclearUltrapower.SOS.ElementarySpectral.delta_eq_half_laplacian line 309
25. theorem OAI.NuclearUltrapower.SOS.ElementarySpectral.delta_nonneg line 314
26. def OAI.NuclearUltrapower.SOS.ElementarySpectral.unitaryRep line 323
27. theorem OAI.NuclearUltrapower.SOS.ElementarySpectral.unitaryRep_coe line 326
28. theorem OAI.NuclearUltrapower.SOS.ElementarySpectral.delta_energy line 329