OAI/Geometry/SurfaceImmersion/Primitive/CircularBoundaryProfiles.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The scalar limits controlling the boundary argument for a circular velocity, in the canonical normal frame read from the five profiles.

  1. def OAI.ClosedSurfaceR4.GeometryPreservation.circularBoundaryProfile line 12
  2. lemma OAI.ClosedSurfaceR4.GeometryPreservation.circularBoundaryProfile_regular line 16
  3. theorem OAI.ClosedSurfaceR4.GeometryPreservation.circularBoundaryProfile_coefficients line 36

    Source documentation

    The mixed coefficient agrees in absolute value with the geometric angular component; the scaled longitudinal coefficient is R * β.

    theorem circularBoundaryProfile_coefficients {X Y C W e₁ e₂ : Vec} {R α β : ℝ}
    (hD : gramDet Y C ≠ 0) (hR : R ≠ 0)
    (h₁ : e₁ ⬝ᵥ e₁ = 1) (h₂ : e₂ ⬝ᵥ e₂ = 1) (horth : e₁ ⬝ᵥ e₂ = 0)
    (hY₁ : Y ⬝ᵥ e₁ = 0) (hY₂ : Y ⬝ᵥ e₂ = 0)
    (hC₁ : C ⬝ᵥ e₁ = 0) (hC₂ : C ⬝ᵥ e₂ = 0) :
    |profileCoefficients (circularBoundaryProfile X Y C W e₁ e₂ R α β) 2| =
      |W ⬝ᵥ angularDirection e₁ e₂ α| ∧
    |profileCoefficients (circularBoundaryProfile X Y C W e₁ e₂ R α β) 3| = |R*β| := by
…

    Mentions: OAI.ClosedSurfaceR4.GeometryPreservation.profileCoefficients, OAI.ClosedSurfaceR4.GeometryPreservation.circularBoundaryProfile

  4. lemma OAI.ClosedSurfaceR4.GeometryPreservation.circularBoundaryProfile_turn_iff line 67