CircleDifferential.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Intrinsic differentials and cutoff modifications of circle coordinates

The differential is computed in a genuine real quotient chart. Local integer transition functions make it independent of the chosen lift. The cutoff staircase descends to the circle and is smooth in the same charts; no global real lift or extra topological input is required.

def OAI.CircleDomainRigidity.FiniteTransfer.circleRepresentative line 21
def OAI.CircleDomainRigidity.FiniteTransfer.circleBranch line 23
theorem OAI.CircleDomainRigidity.FiniteTransfer.coe_circleRepresentative line 26
theorem OAI.CircleDomainRigidity.FiniteTransfer.coe_circleBranch line 29
def OAI.CircleDomainRigidity.FiniteTransfer.circleCut line 32
theorem OAI.CircleDomainRigidity.FiniteTransfer.circleCut_ne line 35
theorem OAI.CircleDomainRigidity.FiniteTransfer.smoothCircleAt_of_local_lift line 48
theorem OAI.CircleDomainRigidity.FiniteTransfer.smoothCircleOn_iff_local_lifts line 73
theorem OAI.CircleDomainRigidity.FiniteTransfer.SmoothCircleOn.continuousOn line 86
def OAI.CircleDomainRigidity.FiniteTransfer.circleFDeriv line 94

theorem OAI.CircleDomainRigidity.FiniteTransfer.circleFDeriv_eq_lift line 100

Source documentation

The intrinsic differential equals that of every continuous local lift, including lifts defined only near the point of differentiation.

theorem circleFDeriv_eq_lift
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {f : E → UnitAddCircle} {u : E → ℝ} {x : E}
    (hf : ContinuousAt f x) (hu : ContinuousAt u x)
    (heq : (fun y => (u y : UnitAddCircle)) =ᶠ[𝓝 x] f) :
    circleFDeriv f x = fderiv ℝ u x := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.circleFDeriv

def OAI.CircleDomainRigidity.FiniteTransfer.circleGradient line 113
theorem OAI.CircleDomainRigidity.FiniteTransfer.circleGradient_eq_lift line 116
def OAI.CircleDomainRigidity.FiniteTransfer.circleCutoff line 124
Source documentation
A unit-additive real modification descends pointwise to the circle.
```
def circleCutoff {X : Type*} (f : X → UnitAddCircle) (χ : X → ℝ) (P : ℝ → ℝ)
    (x : X) : UnitAddCircle :=
…
```
theorem OAI.CircleDomainRigidity.FiniteTransfer.circleCutoff_eq_lift line 128
theorem OAI.CircleDomainRigidity.FiniteTransfer.circleCutoff_eq_of_zero line 144
theorem OAI.CircleDomainRigidity.FiniteTransfer.smoothCircleOn_reciprocal_cutoff line 150
Source documentation
The actual reciprocal-grid cutoff is smooth on every smooth circle coordinate's domain, with the original additive transition functions.
```
theorem smoothCircleOn_reciprocal_cutoff
    {f : (ℝ × ℝ) → UnitAddCircle} {U : Set (ℝ × ℝ)}
    (hf : SmoothCircleOn f U) (χ : (ℝ × ℝ) → ℝ) (hχ : ContDiff ℝ ∞ χ)
    (N : ℕ) {δ : ℝ} (hδ : 0 < δ) (hδh : δ < reciprocalGridStep N / 4) (θ : ℝ) :
    SmoothCircleOn (circleCutoff f χ (shiftedStaircase (reciprocalGridStep N) δ θ)) U := by
…
```
Mentions: OAI.CircleDomainRigidity.FiniteTransfer.SmoothCircleOn, OAI.CircleDomainRigidity.FiniteTransfer.reciprocalGridStep, OAI.CircleDomainRigidity.FiniteTransfer.circleCutoff, OAI.CircleDomainRigidity.FiniteTransfer.shiftedStaircase