OAI/Geometry/RCD/Coordinates/PatchGeometryMonotone.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Enlarging the permissible error of unchanged patch data

  1. def OAI.RegularPointCoordinates.PatchIterationGeometry.monoError line 17

    Source documentation

    Only the allowed mass and energy budget changes; all constructed patches, operators and frozen frames are retained exactly.

    def PatchIterationGeometry.monoError {Ω : Set E} {r0 Theta epsilon delta : ℝ}
    {N : ℕ} {C K L : ℝ} (g : PatchIterationGeometry (ι := ι) Ω r0 Theta epsilon N C K L)
…

    Mentions: OAI.RegularPointCoordinates.PatchIterationGeometry