OAI/Geometry/EinsteinFour/MetricQuadraticPerturbation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A four-dimensional entrywise perturbation estimate for the metric. It converts continuity of the chart metric into almost-isometric norm bounds after freezing an orthonormal frame at one point.

  1. theorem OAI.PositiveEinsteinFour.Geometry.sum_abs_sq_le_four_norm_sq line 17
  2. theorem OAI.PositiveEinsteinFour.Geometry.quadraticForm_entry_bound line 25

    Source documentation

    The factor four is exactly the dimension, so an entrywise bound of δ/4 controls the complete quadratic form by δ.

    theorem quadraticForm_entry_bound (A : Mat4) (δ : ℝ) (hδ : 0 ≤ δ)
    (hA : ∀ i j, |A i j| ≤ δ / 4) (v : FourSpace) :
    |WithLp.ofLp v ⬝ᵥ (A *ᵥ WithLp.ofLp v)| ≤ δ * ‖v‖ ^ 2 := by
…

    Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4

  3. theorem OAI.PositiveEinsteinFour.Geometry.quadraticForm_near_identity line 64