OAI/Geometry/RCD/Harmonic/RadialLinearCoefficient.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Covector operator control from the constructed radial rows

  1. theorem OAI.RegularPointCoordinates.finiteCoefficientMap_relative_bound line 16

    Source documentation

    The covector operator uses the transpose of the matrix acting on coordinate values. A dimension factor suffices to transport its norm estimate, without making any symmetry assumption on the radial matrix.

    theorem finiteCoefficientMap_relative_bound {n : ℕ}
    (N : Euclidean n ≃L[ℝ] Euclidean n) (coeff : Fin n → Euclidean n)
    {epsilon : ℝ} (hepsilon : 0 ≤ epsilon)
    (hbound : ‖Matrix.toEuclideanCLM (n := Fin n) (𝕜 := ℝ)
…

    Mentions: OAI.RegularPointCoordinates.Euclidean