Jointly smooth rephasing by positive periodic densities

Each parameter supplies an actual SmoothLoop.CircleDensity. The inverse is the globally defined monotone inverse already constructed there. Its joint smoothness is proved with the inverse function theorem applied to the triangular map (p, θ) ↦ (p, Φ(p, θ)); no smooth inverse is postulated.

def NavierStokes.ParametricRephase.familyRate {E : Type u_1} (d : E → SmoothLoop.CircleDensity) (z : E × ℝ) : ℝ

Family rate, given by (d z.1).rate z.2.

Equations

• NavierStokes.ParametricRephase.familyRate d z = (d z.1).rate z.2

noncomputable def NavierStokes.ParametricRephase.familyPhase {E : Type u_1} (d : E → SmoothLoop.CircleDensity) (z : E × ℝ) : ℝ

Family phase, given by phaseMap (d z.1) z.2.

Equations

• NavierStokes.ParametricRephase.familyPhase d z = NavierStokes.SmoothLoop.phaseMap (d z.1) z.2

noncomputable def NavierStokes.ParametricRephase.inversePhase {E : Type u_1} (d : E → SmoothLoop.CircleDensity) (z : E × ℝ) : ℝ

Inverse phase, given by (phaseHomeomorph (d z.1)).symm z.2.

Equations

• NavierStokes.ParametricRephase.inversePhase d z = (NavierStokes.SmoothLoop.phaseHomeomorph (d z.1)).symm z.2

noncomputable def NavierStokes.ParametricRephase.forwardMap {E : Type u_1} (d : E → SmoothLoop.CircleDensity) (z : E × ℝ) : E × ℝ

Forward map, given by (z.1, familyPhase d z).

Equations

• NavierStokes.ParametricRephase.forwardMap d z = (z.1, NavierStokes.ParametricRephase.familyPhase d z)

noncomputable def NavierStokes.ParametricRephase.inverseMap {E : Type u_1} (d : E → SmoothLoop.CircleDensity) (z : E × ℝ) : E × ℝ

Inverse map, given by (z.1, inversePhase d z).

Equations

• NavierStokes.ParametricRephase.inverseMap d z = (z.1, NavierStokes.ParametricRephase.inversePhase d z)

theorem NavierStokes.ParametricRephase.inverseMap_forwardMap {E : Type u_1} (d : E → SmoothLoop.CircleDensity) (z : E × ℝ) : inverseMap d (forwardMap d z) = z

theorem NavierStokes.ParametricRephase.forwardMap_inverseMap {E : Type u_1} (d : E → SmoothLoop.CircleDensity) (z : E × ℝ) : forwardMap d (inverseMap d z) = z

theorem NavierStokes.ParametricRephase.forwardMap_bijective {E : Type u_1} (d : E → SmoothLoop.CircleDensity) : Function.Bijective (forwardMap d)

theorem NavierStokes.ParametricRephase.familyPhase_add_fullTurn {E : Type u_1} (d : E → SmoothLoop.CircleDensity) (p : E) (θ : ℝ) : familyPhase d (p, θ + 2 * Real.pi) = familyPhase d (p, θ) + 1

theorem NavierStokes.ParametricRephase.inversePhase_add_one {E : Type u_1} (d : E → SmoothLoop.CircleDensity) (p : E) (φ : ℝ) : inversePhase d (p, φ + 1) = inversePhase d (p, φ) + 2 * Real.pi

theorem NavierStokes.ParametricRephase.familyPhase_partial_hasDerivAt {E : Type u_1} (d : E → SmoothLoop.CircleDensity) (p : E) (θ : ℝ) : HasDerivAt (fun (t : ℝ) => familyPhase d (p, t)) (familyRate d (p, θ)) θ

theorem NavierStokes.ParametricRephase.forwardMap_hasFDerivAt_equiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (d : E → SmoothLoop.CircleDensity) (z : E × ℝ) (hphase : DifferentiableAt ℝ (familyPhase d) z) : ∃ (L : (E × ℝ) ≃L[ℝ] E × ℝ), HasFDerivAt (forwardMap d) (↑L) z

The triangular derivative is a genuine continuous linear equivalence. Its last diagonal entry is the strictly positive density, proved by the FTC.

theorem NavierStokes.ParametricRephase.inverseMap_contDiffAt_of_phase {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (d : E → SmoothLoop.CircleDensity) (z : E × ℝ) (hphase : ContDiffAt ℝ (↑⊤) (familyPhase d) (inverseMap d z)) : ContDiffAt ℝ (↑⊤) (inverseMap d) z

Joint inverse smoothness is derived from the triangular inverse function theorem, then identified with the global inverse using its exact inverse law.

theorem NavierStokes.ParametricRephase.inversePhase_contDiffAt_of_phase {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (d : E → SmoothLoop.CircleDensity) (z : E × ℝ) (hphase : ContDiffAt ℝ (↑⊤) (familyPhase d) (inverseMap d z)) : ContDiffAt ℝ (↑⊤) (inversePhase d) z

theorem NavierStokes.ParametricRephase.inverseMap_contDiffOn_of_phase {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (d : E → SmoothLoop.CircleDensity) (U : Set E) (hU : IsOpen U) (hphase : ContDiffOn ℝ (↑⊤) (familyPhase d) (U ×ˢ Set.univ)) : ContDiffOn ℝ (↑⊤) (inverseMap d) (U ×ˢ Set.univ)

theorem NavierStokes.ParametricRephase.inversePhase_contDiffOn_of_phase {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (d : E → SmoothLoop.CircleDensity) (U : Set E) (hU : IsOpen U) (hphase : ContDiffOn ℝ (↑⊤) (familyPhase d) (U ×ˢ Set.univ)) : ContDiffOn ℝ (↑⊤) (inversePhase d) (U ×ˢ Set.univ)

theorem NavierStokes.ParametricRephase.inversePhase_contDiff_of_phase {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (d : E → SmoothLoop.CircleDensity) (hphase : ContDiff ℝ (↑⊤) (familyPhase d)) : ContDiff ℝ (↑⊤) (inversePhase d)

noncomputable def NavierStokes.ParametricRephase.rephaseFamily {E : Type u_1} {V : Type u_2} (d : E → SmoothLoop.CircleDensity) (f : E × ℝ → V) (z : E × ℝ) : V

Rephase family, given by f (inverseMap d z).

Equations

• NavierStokes.ParametricRephase.rephaseFamily d f z = f (NavierStokes.ParametricRephase.inverseMap d z)

theorem NavierStokes.ParametricRephase.rephaseFamily_periodic {E : Type u_1} {V : Type u_2} (d : E → SmoothLoop.CircleDensity) (f : E × ℝ → V) (p : E) (hf : Function.Periodic (fun (θ : ℝ) => f (p, θ)) (2 * Real.pi)) : Function.Periodic (fun (φ : ℝ) => rephaseFamily d f (p, φ)) 1

theorem NavierStokes.ParametricRephase.rephaseFamily_forwardMap {E : Type u_1} {V : Type u_2} (d : E → SmoothLoop.CircleDensity) (f : E × ℝ → V) (z : E × ℝ) : rephaseFamily d f (forwardMap d z) = f z

theorem NavierStokes.ParametricRephase.rephaseFamily_integral {E : Type u_1} (d : E → SmoothLoop.CircleDensity) (f : E × ℝ → ℝ) (p : E) (hf : Continuous fun (θ : ℝ) => f (p, θ)) : ∫ (φ : ℝ) in 0..1, rephaseFamily d f (p, φ) = ∫ (θ : ℝ) in 0..2 * Real.pi, f (p, θ) * familyRate d (p, θ)

theorem NavierStokes.ParametricRephase.rephaseFamily_contDiffOn_of_phase {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace E] (d : E → SmoothLoop.CircleDensity) (f : E × ℝ → V) (U : Set E) (hU : IsOpen U) (hphase : ContDiffOn ℝ (↑⊤) (familyPhase d) (U ×ˢ Set.univ)) (hf : ContDiffOn ℝ (↑⊤) f (U ×ˢ Set.univ)) : ContDiffOn ℝ (↑⊤) (rephaseFamily d f) (U ×ˢ Set.univ)

noncomputable def NavierStokes.ParametricRephase.parameterJet {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] (F : E × ℝ → V) (k : ℕ) (z : E × ℝ) : E [×k]→L[ℝ] V

Genuine iterated derivatives in the parameter while the last variable is held fixed. This is not a separately postulated family of jets.

Equations

• NavierStokes.ParametricRephase.parameterJet F k z = iteratedFDeriv ℝ k (fun (p : E) => F (p, z.2)) z.1

theorem NavierStokes.ParametricRephase.parameterJet_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] (F : E × ℝ → V) (U : Set E) (hU : IsOpen U) (hF : ContDiffOn ℝ (↑⊤) F (U ×ˢ Set.univ)) (k : ℕ) : ContDiffOn ℝ (↑⊤) (parameterJet F k) (U ×ˢ Set.univ)

Joint smoothness implies joint smoothness of every genuine parameter jet. This supplies the derivative continuity used in compact-interval integration.

theorem NavierStokes.ParametricRephase.intervalIntegral_contDiffOn_of_joint {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [ProperSpace E] (F : E × ℝ → V) (U : Set E) (hU : IsOpen U) (hF : ContDiffOn ℝ (↑⊤) F (U ×ˢ Set.univ)) (a b : ℝ) (hab : a ≤ b) : ContDiffOn ℝ (↑⊤) (fun (p : E) => ∫ (t : ℝ) in a..b, F (p, t)) U

Integration over a fixed compact interval preserves joint smoothness. All derivative domination is derived from compactness in the imported theorem.

theorem NavierStokes.ParametricRephase.familyPhase_unit_interval {E : Type u_1} (d : E → SmoothLoop.CircleDensity) (z : E × ℝ) : familyPhase d z = z.2 * ∫ (t : ℝ) in 0..1, familyRate d (z.1, z.2 * t)

theorem NavierStokes.ParametricRephase.familyPhase_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (d : E → SmoothLoop.CircleDensity) (U : Set E) (hU : IsOpen U) (hrate : ContDiffOn ℝ (↑⊤) (familyRate d) (U ×ˢ Set.univ)) : ContDiffOn ℝ (↑⊤) (familyPhase d) (U ×ˢ Set.univ)

The actual variable-endpoint cumulative integral is jointly smooth. No regularity of that integral is assumed separately from regularity of the density.

theorem NavierStokes.ParametricRephase.inverseMap_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (d : E → SmoothLoop.CircleDensity) (U : Set E) (hU : IsOpen U) (hrate : ContDiffOn ℝ (↑⊤) (familyRate d) (U ×ˢ Set.univ)) : ContDiffOn ℝ (↑⊤) (inverseMap d) (U ×ˢ Set.univ)

Final density-only interface for the joint inverse on an open parameter set.

theorem NavierStokes.ParametricRephase.inversePhase_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (d : E → SmoothLoop.CircleDensity) (U : Set E) (hU : IsOpen U) (hrate : ContDiffOn ℝ (↑⊤) (familyRate d) (U ×ˢ Set.univ)) : ContDiffOn ℝ (↑⊤) (inversePhase d) (U ×ˢ Set.univ)

theorem NavierStokes.ParametricRephase.inversePhase_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (d : E → SmoothLoop.CircleDensity) (hrate : ContDiff ℝ (↑⊤) (familyRate d)) : ContDiff ℝ (↑⊤) (inversePhase d)

theorem NavierStokes.ParametricRephase.rephaseFamily_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ E] (d : E → SmoothLoop.CircleDensity) (f : E × ℝ → V) (U : Set E) (hU : IsOpen U) (hrate : ContDiffOn ℝ (↑⊤) (familyRate d) (U ×ˢ Set.univ)) (hf : ContDiffOn ℝ (↑⊤) f (U ×ˢ Set.univ)) : ContDiffOn ℝ (↑⊤) (rephaseFamily d f) (U ×ˢ Set.univ)

Smooth loops remain jointly smooth under the constructed parameter-dependent phase inverse. Their period becomes one by rephaseFamily_periodic.

theorem NavierStokes.ParametricRephase.rephaseFamily_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ E] (d : E → SmoothLoop.CircleDensity) (f : E × ℝ → V) (hrate : ContDiff ℝ (↑⊤) (familyRate d)) (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (rephaseFamily d f)