OAI/Analysis/CircleDomains/Topology/CircleCovectors.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Smooth covector fields of periodic coordinates

The locally defined circle differential is an ordinary smooth covector field on its open domain. This supplies the tensor used in the same metric construction as for single-valued real coordinates.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.circleFDeriv_eventuallyEq_lift line 20
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.contDiffOn_circleFDeriv line 32
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.contDiffOn_circleGradient line 49
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.circleGradient_eventuallyEq_lift line 57

    Source documentation

    On a local real branch the intrinsic covector field equals the ordinary gradient on a whole neighborhood, not only at its center.

    theorem circleGradient_eventuallyEq_lift
    {f : (ℝ × ℝ) → UnitAddCircle} {u : (ℝ × ℝ) → ℝ} {U : Set (ℝ × ℝ)}
    (hU : IsOpen U) (hf : ContinuousOn f U) (hu : ContDiffOn ℝ ∞ u U)
    (hproj : ∀ y ∈ U, (u y : UnitAddCircle) = f y) {x : ℝ × ℝ} (hx : x ∈ U) :
    circleGradient f =ᶠ[𝓝 x] planarGradient u := by
…

    Mentions: OAI.CircleDomainRigidity.FiniteTransfer.circleGradient, OAI.CircleDomainRigidity.FiniteTransfer.planarGradient