OAI/Analysis/CircleDomains/Sobolev/LiftDifferentials.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Independence of differentials from the chosen real lift

Two continuous real lifts of one circle map differ locally by a fixed integer. Their differentials, and those of the actual reciprocal-grid cutoff modifications, therefore agree. These are local consequences of the real quotient, with no additional published input.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.eventually_lifts_differ_by_integer line 22
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.fderiv_lifts_eq line 43
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.planarGradient_lifts_eq line 52
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.map_add_int_of_add_one line 58
  5. theorem OAI.CircleDomainRigidity.FiniteTransfer.cutoffStaircase_add_int line 69
  6. theorem OAI.CircleDomainRigidity.FiniteTransfer.eventually_cutoff_lifts_differ_by_integer line 77

    Source documentation

    Cutoff modification preserves the same local integer transition between two lifts, not just equality of the projected circle maps.

    theorem eventually_cutoff_lifts_differ_by_integer
    {X : Type*} [TopologicalSpace X] {u v : X โ†’ โ„} {x : X}
    (hu : ContinuousAt u x) (hv : ContinuousAt v x)
    (hproj : (fun y => (u y : UnitAddCircle)) =แถ [๐“ x] fun y => (v y : UnitAddCircle))
    (ฯ‡ : X โ†’ โ„) {P : โ„ โ†’ โ„} (hP : โˆ€ r, P (r + 1) = P r + 1) :
    โˆƒ m : โ„ค, cutoffStaircase u ฯ‡ P =แถ [๐“ x] fun y => cutoffStaircase v ฯ‡ P y + (m : โ„) := by
โ€ฆ

    Mentions: OAI.CircleDomainRigidity.FiniteTransfer.cutoffStaircase

  7. theorem OAI.CircleDomainRigidity.FiniteTransfer.fderiv_cutoff_lifts_eq line 88
  8. theorem OAI.CircleDomainRigidity.FiniteTransfer.planarGradient_reciprocal_cutoff_lifts_eq line 99

    Source documentation

    The actual selected staircase therefore defines one differential independently of all choices of continuous real branch.

    theorem planarGradient_reciprocal_cutoff_lifts_eq
    {u v : (โ„ ร— โ„) โ†’ โ„} {z : โ„ ร— โ„} (hu : ContinuousAt u z) (hv : ContinuousAt v z)
    (hproj : (fun y => (u y : UnitAddCircle)) =แถ [๐“ z] fun y => (v y : UnitAddCircle))
    (ฯ‡ : (โ„ ร— โ„) โ†’ โ„) (N : โ„•) (ฮด ฮธ : โ„) :
    planarGradient (cutoffStaircase u ฯ‡ (shiftedStaircase (reciprocalGridStep N) ฮด ฮธ)) z =
      planarGradient (cutoffStaircase v ฯ‡ (shiftedStaircase (reciprocalGridStep N) ฮด ฮธ)) z := by
โ€ฆ

    Mentions: OAI.CircleDomainRigidity.FiniteTransfer.planarGradient, OAI.CircleDomainRigidity.FiniteTransfer.cutoffStaircase, OAI.CircleDomainRigidity.FiniteTransfer.shiftedStaircase, OAI.CircleDomainRigidity.FiniteTransfer.reciprocalGridStep