OneSidedCauchy.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Cauchy--Schwarz for the one-sided character interaction

The long-variable unary restriction is removed before extending its prior. The diagonal short-variable pairs cost only their maximum atom.

theorem OAI.Ostmann.weighted_family_energy_le_atom line 16

theorem OAI.Ostmann.one_sided_cauchy_bound line 72

Source documentation

Bounded unary factors on both variables are permitted. The extension measure need not have mass one; its diagonal cost is recorded in D.

theorem one_sided_cauchy_bound {A B : Type*} [Fintype A] [Fintype B]
    (μ η : A → ℝ) (ν : B → ℝ) (U : A → ℂ) (V : B → ℂ) (F : B → A → ℂ)
    (C α D ε : ℝ) (hC : 0 ≤ C) (hα : 0 ≤ α) (hD : 0 ≤ D) (hε : 0 ≤ ε)
    (hμ : ∀ p, 0 ≤ μ p) (hmassμ : ∑ p, μ p ≤ 1)
    (hdom : ∀ p, μ p ≤ C * η p)
    (hν : ∀ q, 0 ≤ ν q) (hmassν : ∑ q, ν q ≤ 1) (hatom : ∀ q, ν q ≤ α)
    (hU : ∀ p, ‖U p‖ ≤ 1) (hV : ∀ q, ‖V q‖ ≤ 1)
    (hcorr : ∀ q r, ‖∑ p, (η p : ℂ) * (F q p * conj (F r p))‖ ≤
      if q = r then D else ε) :
    ‖∑ p, (μ p : ℂ) * (U p * ∑ q, (ν q : ℂ) * V q * F q p)‖ ^ 2 ≤
      C * (α * D + ε) := by
…

theorem OAI.Ostmann.diagonal_correlation_envelope line 101

theorem OAI.Ostmann.one_sided_cauchy_of_offdiagonal line 120

Source documentation

Only the off-diagonal character correlations require cancellation. The diagonal estimate follows from the envelope and maximum short atom.

theorem one_sided_cauchy_of_offdiagonal {A B : Type*} [Fintype A] [Fintype B]
    (μ η : A → ℝ) (ν : B → ℝ) (U : A → ℂ) (V : B → ℂ) (F : B → A → ℂ)
    (C α H B₀ ε : ℝ) (hC : 0 ≤ C) (hα : 0 ≤ α) (hH : 0 ≤ H) (hε : 0 ≤ ε)
    (hμ : ∀ p, 0 ≤ μ p) (hmassμ : ∑ p, μ p ≤ 1)
    (hdom : ∀ p, μ p ≤ C * η p) (hη : ∀ p, 0 ≤ η p) (hmassη : ∑ p, η p ≤ H)
    (hν : ∀ q, 0 ≤ ν q) (hmassν : ∑ q, ν q ≤ 1) (hatom : ∀ q, ν q ≤ α)
    (hU : ∀ p, ‖U p‖ ≤ 1) (hV : ∀ q, ‖V q‖ ≤ 1) (hF : ∀ q p, ‖F q p‖ ≤ B₀)
    (hoff : ∀ q r, q ≠ r →
      ‖∑ p, (η p : ℂ) * (F q p * conj (F r p))‖ ≤ ε) :
    ‖∑ p, (μ p : ℂ) * (U p * ∑ q, (ν q : ℂ) * V q * F q p)‖ ^ 2 ≤
      C * (α * (H * B₀ ^ 2) + ε) := by
…