SymmetricDomination.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Bilinear estimates from domination of symmetric quadratic forms

theorem OAI.RegularPointCoordinates.symmetric_domination_cauchy_schwarz line 15
Source documentation
Domination of the absolute quadratic form gives Cauchy--Schwarz with the dominating form in both directions. The dominated operator may be signed.
```
theorem symmetric_domination_cauchy_schwarz (D P : E →L[ℝ] E)
    (hD : D.IsSymmetric) (hdom : ∀ v, |⟪v, D v⟫_ℝ| ≤ ⟪v, P v⟫_ℝ)
    (v w : E) :
    ⟪v, D w⟫_ℝ ^ 2 ≤ ⟪v, P v⟫_ℝ * ⟪w, P w⟫_ℝ := by
…
```

theorem OAI.RegularPointCoordinates.symmetric_domination_mixed line 37

Source documentation

A small upper bound for the dominating form in one direction gives the asymmetric bound used by the heat/mean source comparison.

theorem symmetric_domination_mixed (D P Q : E →L[ℝ] E)
    (hD : D.IsSymmetric) (hP : P.IsPositive)
    (hdom : ∀ v, |⟪v, D v⟫_ℝ| ≤ ⟪v, P v⟫_ℝ)
    {ε : ℝ} (hsmall : ∀ v, ⟪v, P v⟫_ℝ ≤ ε * ⟪v, Q v⟫_ℝ) (v w : E) :
    ⟪v, D w⟫_ℝ ^ 2 ≤ ε * ⟪v, P v⟫_ℝ * ⟪w, Q w⟫_ℝ := by
…