OAI/Analysis/CircleDomains/Transfer/PeriodicFilling.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Integer-translated fillings on the pulled-back circle cover

Section 2, Step 4, of the Koebe manuscript fills one sheet over each filling disk and uses its integer translates on all other sheets. Here the cover is the actual pullback of ℝ → ℝ/ℤ by the original circle coordinate. The filled real function is the original height plus the base correction g - u on each disk. Thus it has exactly the original deck increments and projects to the circle map already constructed by CirclePatching.

The differentials on every sheet are those of the selected real filling. No additional lifting, period, or winding input is assumed.

  1. def OAI.CircleDomainRigidity.FiniteTransfer.CircleLiftCover line 31

    Source documentation

    The literal pullback of the universal real cover by a circle map.

    def CircleLiftCover {X : Type*} (f : X → UnitAddCircle) :=
…
  2. instance OAI.CircleDomainRigidity.FiniteTransfer.(instance at line 34) line 34
  3. def OAI.CircleDomainRigidity.FiniteTransfer.CircleLiftCover.base line 38
  4. def OAI.CircleDomainRigidity.FiniteTransfer.CircleLiftCover.height line 41
  5. theorem OAI.CircleDomainRigidity.FiniteTransfer.CircleLiftCover.height_projects line 44
  6. def OAI.CircleDomainRigidity.FiniteTransfer.CircleLiftCover.translate line 48

    Source documentation

    Integer translations act on this pullback without changing the base.

    def CircleLiftCover.translate {X : Type*} {f : X → UnitAddCircle}
    (m : ℤ) (p : CircleLiftCover f) : CircleLiftCover f :=
…

    Mentions: OAI.CircleDomainRigidity.FiniteTransfer.CircleLiftCover

  7. theorem OAI.CircleDomainRigidity.FiniteTransfer.CircleLiftCover.base_translate line 53
  8. theorem OAI.CircleDomainRigidity.FiniteTransfer.CircleLiftCover.height_translate line 56
  9. theorem OAI.CircleDomainRigidity.FiniteTransfer.CircleLiftCover.translate_zero line 59
  10. theorem OAI.CircleDomainRigidity.FiniteTransfer.CircleLiftCover.translate_add line 65
  11. theorem OAI.CircleDomainRigidity.FiniteTransfer.CircleLiftCover.continuous_base line 71
  12. theorem OAI.CircleDomainRigidity.FiniteTransfer.CircleLiftCover.continuous_height line 75
  13. theorem OAI.CircleDomainRigidity.FiniteTransfer.CircleLiftCover.continuous_translate line 79
  14. def OAI.CircleDomainRigidity.FiniteTransfer.CircleLiftCover.cutoffLift line 88

    Source documentation

    The actual cutoff sends the original pullback cover to the pullback of the modified circle coordinate, over the identity of the base.

    def CircleLiftCover.cutoffLift {X : Type*} {f : X → UnitAddCircle}
    (χ : X → ℝ) (P : ℝ → ℝ) (hP : ∀ r, P (r + 1) = P r + 1)
    (p : CircleLiftCover f) : CircleLiftCover (circleCutoff f χ P) :=
…

    Mentions: OAI.CircleDomainRigidity.FiniteTransfer.CircleLiftCover, OAI.CircleDomainRigidity.FiniteTransfer.circleCutoff

  15. theorem OAI.CircleDomainRigidity.FiniteTransfer.CircleLiftCover.base_cutoffLift line 94
  16. theorem OAI.CircleDomainRigidity.FiniteTransfer.CircleLiftCover.cutoffLift_translate line 98
  17. theorem OAI.CircleDomainRigidity.FiniteTransfer.CircleLiftCover.continuous_cutoffLift line 111
  18. def OAI.CircleDomainRigidity.FiniteTransfer.fillingCorrection line 121

    Source documentation

    The change on a selected base disk; it is zero off the disks.

    def fillingCorrection {X I : Type*} (D : I → Set X) (u g : I → X → ℝ) : X → ℝ :=
…
  19. def OAI.CircleDomainRigidity.FiniteTransfer.periodicFilledValue line 125

    Source documentation

    Fill on one sheet and translate on every other sheet.

    def periodicFilledValue {X I : Type*} (f : X → UnitAddCircle)
    (D : I → Set X) (u g : I → X → ℝ) (p : CircleLiftCover f) : ℝ :=
…

    Mentions: OAI.CircleDomainRigidity.FiniteTransfer.CircleLiftCover

  20. theorem OAI.CircleDomainRigidity.FiniteTransfer.periodicFilledValue_translate line 131

    Source documentation

    Every integer deck increment, in particular the positive period one, is retained by the actual filling formula.

    theorem periodicFilledValue_translate {X I : Type*} (f : X → UnitAddCircle)
    (D : I → Set X) (u g : I → X → ℝ) (p : CircleLiftCover f) (m : ℤ) :
    periodicFilledValue f D u g (p.translate m) =
      periodicFilledValue f D u g p + (m : ℝ) := by
…

    Mentions: OAI.CircleDomainRigidity.FiniteTransfer.CircleLiftCover, OAI.CircleDomainRigidity.FiniteTransfer.periodicFilledValue

  21. theorem OAI.CircleDomainRigidity.FiniteTransfer.periodicCutoffFilledValue_translate line 141

    Source documentation

    Cutoff followed by filling retains the original cover's deck action, not just the action on a separately chosen cover of the modified map.

    theorem periodicCutoffFilledValue_translate {X I : Type*} (f : X → UnitAddCircle)
    (χ : X → ℝ) (P : ℝ → ℝ) (hP : ∀ r, P (r + 1) = P r + 1)
    (D : I → Set X) (u g : I → X → ℝ) (p : CircleLiftCover f) (m : ℤ) :
    periodicFilledValue (circleCutoff f χ P) D u g ((p.translate m).cutoffLift χ P hP) =
      periodicFilledValue (circleCutoff f χ P) D u g (p.cutoffLift χ P hP) + (m : ℝ) := by
…

    Mentions: OAI.CircleDomainRigidity.FiniteTransfer.CircleLiftCover, OAI.CircleDomainRigidity.FiniteTransfer.periodicFilledValue, OAI.CircleDomainRigidity.FiniteTransfer.circleCutoff

  22. theorem OAI.CircleDomainRigidity.FiniteTransfer.periodicFilledValue_inside line 148
  23. theorem OAI.CircleDomainRigidity.FiniteTransfer.periodicFilledValue_outside line 156
  24. theorem OAI.CircleDomainRigidity.FiniteTransfer.periodicFilledValue_inside_integer line 163

    Source documentation

    Each sheet differs from the selected filling by an actual integer.

    theorem periodicFilledValue_inside_integer {X I : Type*} (f : X → UnitAddCircle)
    (D : I → Set X) (u g : I → X → ℝ) (hdisj : Pairwise (Disjoint on D))
    (hu : ∀ i x, x ∈ D i → (u i x : UnitAddCircle) = f x)
    {i : I} {p : CircleLiftCover f} (hp : p.base ∈ D i) :
    ∃ m : ℤ, periodicFilledValue f D u g p = g i p.base + (m : ℝ) := by
…

    Mentions: OAI.CircleDomainRigidity.FiniteTransfer.CircleLiftCover, OAI.CircleDomainRigidity.FiniteTransfer.periodicFilledValue

  25. theorem OAI.CircleDomainRigidity.FiniteTransfer.periodicFilledValue_projects line 176

    Source documentation

    The deck-compatible real filling projects to precisely the already constructed circle patch.

    theorem periodicFilledValue_projects {X I : Type*} (f : X → UnitAddCircle)
    (D : I → Set X) (u g : I → X → ℝ) (hdisj : Pairwise (Disjoint on D))
    (hu : ∀ i x, x ∈ D i → (u i x : UnitAddCircle) = f x)
    (p : CircleLiftCover f) :
    (periodicFilledValue f D u g p : UnitAddCircle) =
      patchOpenRegions D (fun i x => (g i x : UnitAddCircle)) f p.base := by
…

    Mentions: OAI.CircleDomainRigidity.FiniteTransfer.CircleLiftCover, OAI.CircleDomainRigidity.FiniteTransfer.periodicFilledValue, OAI.CircleDomainRigidity.FiniteTransfer.patchOpenRegions

  26. theorem OAI.CircleDomainRigidity.FiniteTransfer.periodicCutoffFilledValue_projects line 194

    Source documentation

    The complete cutoff-and-filling formula projects to the actual circle patch, using the original local branches as input.

    theorem periodicCutoffFilledValue_projects {X I : Type*} (f : X → UnitAddCircle)
    (χ : X → ℝ) (P : ℝ → ℝ) (hP : ∀ r, P (r + 1) = P r + 1)
    (D : I → Set X) (u g : I → X → ℝ) (hdisj : Pairwise (Disjoint on D))
    (hu : ∀ i x, x ∈ D i → (u i x : UnitAddCircle) = f x) (p : CircleLiftCover f) :
    (periodicFilledValue (circleCutoff f χ P) D
      (fun i => cutoffStaircase (u i) χ P) g (p.cutoffLift χ P hP) : UnitAddCircle) =
      patchOpenRegions D (fun i x => (g i x : UnitAddCircle)) (circleCutoff f χ P) p.base := by
…

    Mentions: OAI.CircleDomainRigidity.FiniteTransfer.CircleLiftCover, OAI.CircleDomainRigidity.FiniteTransfer.periodicFilledValue, OAI.CircleDomainRigidity.FiniteTransfer.circleCutoff, OAI.CircleDomainRigidity.FiniteTransfer.cutoffStaircase, OAI.CircleDomainRigidity.FiniteTransfer.patchOpenRegions

  27. theorem OAI.CircleDomainRigidity.FiniteTransfer.contDiff_fillingCorrection line 207

    Source documentation

    Boundary collar agreement makes the base correction globally smooth. Only the local real branches on the disks are needed.

    theorem contDiff_fillingCorrection
    {E I : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype I]
    (D : I → Set E) (hD : ∀ i, IsOpen (D i)) (hdisj : Pairwise (Disjoint on D))
    (u g : I → E → ℝ) (hu : ∀ i, ContDiffOn ℝ ∞ (u i) (D i))
    (hg : ∀ i, ContDiffOn ℝ ∞ (g i) (D i))
    (hagree : ∀ i x, x ∈ frontier (D i) → g i =ᶠ[𝓝 x] u i) :
    ContDiff ℝ ∞ (fillingCorrection D u g) := by
…

    Mentions: OAI.CircleDomainRigidity.FiniteTransfer.fillingCorrection

  28. theorem OAI.CircleDomainRigidity.FiniteTransfer.eventually_filledBranch_eq_add_int line 224

    Source documentation

    A branch on any other sheet has the selected real filling's derivative.

    theorem eventually_filledBranch_eq_add_int
    {E I : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (D : I → Set E) (hD : ∀ i, IsOpen (D i)) (hdisj : Pairwise (Disjoint on D))
    (u g : I → E → ℝ) {v : E → ℝ} {i : I} {x : E} (hx : x ∈ D i)
    (hv : ContinuousAt v x) (hu : ContinuousAt (u i) x)
    (hproj : (fun y => (v y : UnitAddCircle)) =ᶠ[𝓝 x] fun y => (u i y : UnitAddCircle)) :
    ∃ m : ℤ, (fun y => v y + fillingCorrection D u g y) =ᶠ[𝓝 x]
      fun y => g i y + (m : ℝ) := by
…

    Mentions: OAI.CircleDomainRigidity.FiniteTransfer.fillingCorrection

  29. theorem OAI.CircleDomainRigidity.FiniteTransfer.fderiv_filledBranch_inside line 238
  30. theorem OAI.CircleDomainRigidity.FiniteTransfer.planarGradient_filledBranch_inside line 248
  31. theorem OAI.CircleDomainRigidity.FiniteTransfer.wedge_filledBranches_inside line 258

    Source documentation

    Rank-one wedge identities are unchanged on arbitrary lifted sheets.

    theorem wedge_filledBranches_inside
    {I : Type*} (D : I → Set (ℝ × ℝ)) (hD : ∀ i, IsOpen (D i))
    (hdisj : Pairwise (Disjoint on D)) (u g u' g' : I → (ℝ × ℝ) → ℝ)
    {v w : (ℝ × ℝ) → ℝ} {i : I} {x : ℝ × ℝ} (hx : x ∈ D i)
    (hv : ContinuousAt v x) (hw : ContinuousAt w x)
    (hu : ContinuousAt (u i) x) (hu' : ContinuousAt (u' i) x)
    (hvproj : (fun y => (v y : UnitAddCircle)) =ᶠ[𝓝 x] fun y => (u i y : UnitAddCircle))
    (hwproj : (fun y => (w y : UnitAddCircle)) =ᶠ[𝓝 x] fun y => (u' i y : UnitAddCircle)) :
    planarWedge (planarGradient (fun y => v y + fillingCorrection D u g y) x)
      (planarGradient (fun y => w y + fillingCorrection D u' g' y) x) =
        planarWedge (planarGradient (g i) x) (planarGradient (g' i) x) := by
…

    Mentions: OAI.CircleDomainRigidity.FiniteTransfer.planarWedge, OAI.CircleDomainRigidity.FiniteTransfer.planarGradient, OAI.CircleDomainRigidity.FiniteTransfer.fillingCorrection

  32. theorem OAI.CircleDomainRigidity.FiniteTransfer.periodicFilledValue_circuit_increment line 274

    Source documentation

    Endpoint increments on lifted circuits retain their original deck number, including zero for a closed lift and one for a positive lift.

    theorem periodicFilledValue_circuit_increment {X I : Type*} (f : X → UnitAddCircle)
    (D : I → Set X) (u g : I → X → ℝ)
    (γ : unitInterval → CircleLiftCover f) (m : ℤ)
    (hγ : γ 1 = (γ 0).translate m) :
    periodicFilledValue f D u g (γ 1) - periodicFilledValue f D u g (γ 0) = (m : ℝ) := by
…

    Mentions: OAI.CircleDomainRigidity.FiniteTransfer.CircleLiftCover, OAI.CircleDomainRigidity.FiniteTransfer.periodicFilledValue

  33. theorem OAI.CircleDomainRigidity.FiniteTransfer.isLocallyConstant_real_lift_difference line 283

    Source documentation

    The real difference of two continuous lifts is locally constant.

    theorem isLocallyConstant_real_lift_difference
    {X : Type*} [TopologicalSpace X] {u v : X → ℝ}
    (hu : Continuous u) (hv : Continuous v)
    (hproj : ∀ x, (u x : UnitAddCircle) = (v x : UnitAddCircle)) :
    IsLocallyConstant (fun x => u x - v x) := by
…
  34. theorem OAI.CircleDomainRigidity.FiniteTransfer.real_lift_path_increment_eq line 296

    Source documentation

    Endpoint differences of continuous real lifts of one path agree.

    theorem real_lift_path_increment_eq (u v : C(unitInterval, ℝ))
    (hproj : ∀ t, (u t : UnitAddCircle) = (v t : UnitAddCircle)) :
    u 1 - u 0 = v 1 - v 0 := by
…
  35. def OAI.CircleDomainRigidity.FiniteTransfer.realCirclePathLift line 305

    Source documentation

    Canonical lift, used only to make the path increment independent of the choice of real branch.

    def realCirclePathLift (γ : C(unitInterval, UnitAddCircle)) : C(unitInterval, ℝ) :=
…
  36. theorem OAI.CircleDomainRigidity.FiniteTransfer.realCirclePathLift_projects line 309
  37. def OAI.CircleDomainRigidity.FiniteTransfer.circlePathIncrement line 315

    Source documentation

    Winding measured in turns; on a loop it is an integer.

    def circlePathIncrement (γ : C(unitInterval, UnitAddCircle)) : ℝ :=
…
  38. theorem OAI.CircleDomainRigidity.FiniteTransfer.circlePathIncrement_eq_lift line 318
  39. theorem OAI.CircleDomainRigidity.FiniteTransfer.circlePathIncrement_integer line 325
  40. theorem OAI.CircleDomainRigidity.FiniteTransfer.circlePathIncrement_zero_of_closed_lift line 336

    Source documentation

    A circuit carrying a single-valued real branch has zero winding.

    theorem circlePathIncrement_zero_of_closed_lift (γ : C(unitInterval, UnitAddCircle))
    (u : C(unitInterval, ℝ)) (hu : ∀ t, (u t : UnitAddCircle) = γ t)
    (hclosed : u 1 = u 0) : circlePathIncrement γ = 0 := by
…

    Mentions: OAI.CircleDomainRigidity.FiniteTransfer.circlePathIncrement

  41. theorem OAI.CircleDomainRigidity.FiniteTransfer.circlePathIncrement_zero_of_branch line 343

    Source documentation

    In particular, every nonsingular terminal circuit admitting the existing real branch on its collar has period zero.

    theorem circlePathIncrement_zero_of_branch
    {X : Type*} [TopologicalSpace X] (c : C(unitInterval, X)) (hc : c 1 = c 0)
    {O : Set X} (u : X → ℝ) (hu : ContinuousOn u O) (hO : ∀ t, c t ∈ O)
    (γ : C(unitInterval, UnitAddCircle)) (hproj : ∀ t, (u (c t) : UnitAddCircle) = γ t) :
    circlePathIncrement γ = 0 := by
…

    Mentions: OAI.CircleDomainRigidity.FiniteTransfer.circlePathIncrement

  42. theorem OAI.CircleDomainRigidity.FiniteTransfer.circlePathIncrement_eq_integral_deriv line 355

    Source documentation

    For a continuously differentiable parametrized lift, the path increment is the integral of its differential. This identifies the deck calculation with the period appearing in the manuscript.

    theorem circlePathIncrement_eq_integral_deriv (γ : C(unitInterval, UnitAddCircle))
    (u : ℝ → ℝ) (hu : ContDiffOn ℝ 1 u (uIcc (0 : ℝ) 1))
    (hproj : ∀ t : unitInterval, (u t : UnitAddCircle) = γ t) :
    circlePathIncrement γ = ∫ t in (0 : ℝ)..1, deriv u t := by
…

    Mentions: OAI.CircleDomainRigidity.FiniteTransfer.circlePathIncrement

  43. theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_filled_circle_circuit_with_increment line 368

    Source documentation

    A lifted circuit ending on sheet m projects to a genuine closed circuit of the patched circle map with winding m. The continuous real lift is constructed from the original height and the base correction.

    theorem exists_filled_circle_circuit_with_increment
    {X I : Type*} [TopologicalSpace X]
    (f : X → UnitAddCircle) (D : I → Set X) (u g : I → X → ℝ)
    (hdisj : Pairwise (Disjoint on D))
    (hu : ∀ i x, x ∈ D i → (u i x : UnitAddCircle) = f x)
    (hcorr : Continuous (fillingCorrection D u g))
    (c : C(unitInterval, CircleLiftCover f)) (m : ℤ)
    (hc : c 1 = (c 0).translate m) :
    ∃ γ : C(unitInterval, UnitAddCircle),
      (∀ t, γ t = patchOpenRegions D (fun i x => (g i x : UnitAddCircle)) f (c t).base) ∧
      γ 1 = γ 0 ∧ circlePathIncrement γ = (m : ℝ) := by
…

    Mentions: OAI.CircleDomainRigidity.FiniteTransfer.fillingCorrection, OAI.CircleDomainRigidity.FiniteTransfer.CircleLiftCover, OAI.CircleDomainRigidity.FiniteTransfer.patchOpenRegions, OAI.CircleDomainRigidity.FiniteTransfer.circlePathIncrement

  44. theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_cutoff_filled_circle_circuit_with_increment line 394

    Source documentation

    The same winding statement for the full staircase cutoff followed by the filling, starting with a circuit on the original pullback cover.

    theorem exists_cutoff_filled_circle_circuit_with_increment
    {X I : Type*} [TopologicalSpace X]
    (f : X → UnitAddCircle) (χ : X → ℝ) (P : ℝ → ℝ)
    (hP : ∀ r, P (r + 1) = P r + 1) (hχ : Continuous χ) (hPc : Continuous P)
    (D : I → Set X) (u g : I → X → ℝ) (hdisj : Pairwise (Disjoint on D))
    (hu : ∀ i x, x ∈ D i → (u i x : UnitAddCircle) = f x)
    (hcorr : Continuous (fillingCorrection D (fun i => cutoffStaircase (u i) χ P) g))
    (c : C(unitInterval, CircleLiftCover f)) (m : ℤ)
    (hc : c 1 = (c 0).translate m) :
    ∃ γ : C(unitInterval, UnitAddCircle),
      (∀ t, γ t = patchOpenRegions D (fun i x => (g i x : UnitAddCircle))
        (circleCutoff f χ P) (c t).base) ∧
…

    Mentions: OAI.CircleDomainRigidity.FiniteTransfer.fillingCorrection, OAI.CircleDomainRigidity.FiniteTransfer.cutoffStaircase, OAI.CircleDomainRigidity.FiniteTransfer.CircleLiftCover, OAI.CircleDomainRigidity.FiniteTransfer.patchOpenRegions, OAI.CircleDomainRigidity.FiniteTransfer.circleCutoff