BilinearDiagonalBound.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A sharp mixed bound from diagonal bounds and a positive Gram form

theorem OAI.RegularPointCoordinates.bilinear_mixed_bound_of_diagonal line 14

Source documentation

Diagonal domination of a symmetric form by a positive Gram form controls its mixed entries, including when the Gram form is degenerate.

theorem bilinear_mixed_bound_of_diagonal
    (P H : Euclidean m →ₗ[ℝ] Euclidean m →ₗ[ℝ] ℝ)
    (hP : ∀ a b, P a b=P b a) (hpos : ∀ a, 0≤P a a)
    (hH : ∀ a b, H a b=H b a) (C : ℝ) (hC : 0≤C)
    (hdiag : ∀ a, |H a a|≤C*P a a) (a b : Euclidean m) :
    (H a b)^2≤C^2*P a a*P b b := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean

theorem OAI.RegularPointCoordinates.bilinear_mixed_sq_bound_of_diagonal line 74

Source documentation

The square form of the diagonal estimate gives the same sharp mixed estimate, with no division by the density or by a Gram eigenvalue.

theorem bilinear_mixed_sq_bound_of_diagonal
    (P H : Euclidean m →ₗ[ℝ] Euclidean m →ₗ[ℝ] ℝ)
    (hP : ∀ a b, P a b=P b a) (hpos : ∀ a, 0≤P a a)
    (hH : ∀ a b, H a b=H b a) (B : ℝ) (hB : 0≤B)
    (hdiag : ∀ a, (H a a)^2≤B*(P a a)^2) (a b : Euclidean m) :
    (H a b)^2≤B*P a a*P b b := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean