PositiveForms.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Directional estimates for positive local mass forms

These are the two positive-matrix inequalities in re:positive-matrix-bound, in coordinates where the frozen metric is the identity. Positivity permits singular mass forms; no inverse of a local mass matrix is used.

theorem OAI.RegularPointCoordinates.positive_form_cauchy_schwarz line 22

Source documentation

Cauchy--Schwarz for a possibly degenerate positive quadratic form.

theorem positive_form_cauchy_schwarz {D : E →L[ℝ] E} (hD : D.IsPositive) (x y : E) :
    ⟪x, D y⟫_ℝ ^ 2 ≤ ⟪x, D x⟫_ℝ * ⟪y, D y⟫_ℝ := by
…

theorem OAI.RegularPointCoordinates.positive_form_inner_abs_le line 38

Source documentation

The directional Cauchy--Schwarz inequality in the form used for cutoffs.

theorem positive_form_inner_abs_le {D : E →L[ℝ] E} (hD : D.IsPositive) (x y : E) :
    |⟪x, D y⟫_ℝ| ≤ Real.sqrt ⟪x, D x⟫_ℝ * Real.sqrt ⟪y, D y⟫_ℝ := by
…

theorem OAI.RegularPointCoordinates.positive_form_norm_sq_le line 49

Source documentation

A small positive form controls the Euclidean norm of its value by its own directional energy.

theorem positive_form_norm_sq_le {D : E →L[ℝ] E} (hD : D.IsPositive)
    {epsilon : ℝ} (hbound : ∀ v, ⟪v, D v⟫_ℝ ≤ epsilon * ‖v‖ ^ 2) (w : E) :
    ‖D w‖ ^ 2 ≤ epsilon * ⟪w, D w⟫_ℝ := by
…

theorem OAI.RegularPointCoordinates.positive_form_norm_le line 64

Source documentation

The norm estimate in square-root form, as used for the patch field.

theorem positive_form_norm_le {D : E →L[ℝ] E} (hD : D.IsPositive)
    {epsilon : ℝ} (hepsilon : 0 ≤ epsilon)
    (hbound : ∀ v, ⟪v, D v⟫_ℝ ≤ epsilon * ‖v‖ ^ 2) (w : E) :
    ‖D w‖ ≤ Real.sqrt epsilon * Real.sqrt ⟪w, D w⟫_ℝ := by
…