LeanPool.NavierStokesAndEuler.Euler.CylinderDescentJets

Descended cover tensors are the actual local spatial derivatives on the cylinder. Their composition is the literal finite Taylor composition used by the cylinder L² estimate.

source

theorem EulerCylinderCoverDescent.iteratedFDeriv_deck (P : ℝ) {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (f : EulerLiftedGradientSpace.LiftTangent → W) (hperiod : ∀ (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent), f (z.1, ↑c + z.2) = f z) (n : ℕ) (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent) :

iteratedFDeriv ℝ n f (z.1, ↑c + z.2) = iteratedFDeriv ℝ n f z

source

noncomputable def EulerCylinderCoverDescent.jetSeries (P : ℝ) [Fact (0 < P)] {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (f : EulerLiftedGradientSpace.LiftTangent → W) (q : EulerLiftedGradientSpace.LiftDomain P) :

FormalMultilinearSeries ℝ EulerLiftedGradientSpace.LiftTangent W

Jet series, defined pointwise by descend P (iteratedFDeriv ℝ n f) q.

Equations

EulerCylinderCoverDescent.jetSeries P f q n = EulerCylinderCoverDescent.descend P (iteratedFDeriv ℝ n f) q

Instances For

source

theorem EulerCylinderCoverDescent.jetSeries_cover (P : ℝ) [Fact (0 < P)] {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (f : EulerLiftedGradientSpace.LiftTangent → W) (hperiod : ∀ (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent), f (z.1, ↑c + z.2) = f z) (n : ℕ) (z : EulerLiftedGradientSpace.LiftTangent) :

jetSeries P f (EulerLiftedGradientSpace.coveringMap P z) n = iteratedFDeriv ℝ n f z

source

theorem EulerCylinderCoverDescent.localFieldLift_descend_cover (P : ℝ) [Fact (0 < P)] {W : Type u_1} (f : EulerLiftedGradientSpace.LiftTangent → W) (hperiod : ∀ (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent), f (z.1, ↑c + z.2) = f z) (z : EulerLiftedGradientSpace.LiftTangent) :

EulerMetricTransport.localFieldLift P (descend P f) (EulerLiftedGradientSpace.coveringMap P z) = fun (h : EulerLiftedGradientSpace.LiftTangent) => f (z + h)

source

theorem EulerCylinderCoverDescent.descend_smooth (P : ℝ) [Fact (0 < P)] {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (f : EulerLiftedGradientSpace.LiftTangent → W) (hperiod : ∀ (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent), f (z.1, ↑c + z.2) = f z) (hf : ContDiff ℝ (↑⊤) f) (q : EulerLiftedGradientSpace.LiftDomain P) :

ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (descend P f) q)

source

theorem EulerCylinderCoverDescent.jetSeries_eq_local (P : ℝ) [Fact (0 < P)] {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (f : EulerLiftedGradientSpace.LiftTangent → W) (hperiod : ∀ (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent), f (z.1, ↑c + z.2) = f z) (q : EulerLiftedGradientSpace.LiftDomain P) (n : ℕ) :

jetSeries P f q n = iteratedFDeriv ℝ n (EulerMetricTransport.localFieldLift P (descend P f) q) 0

source

theorem EulerCylinderCoverDescent.jetSeries_joint_continuous (P : ℝ) [Fact (0 < P)] {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] {K : Type u_2} [TopologicalSpace K] (F : K → EulerLiftedGradientSpace.LiftTangent → W) (hF : ∀ (t : K) (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent), F t (z.1, ↑c + z.2) = F t z) (n : ℕ) (hJ : Continuous fun (z : K × EulerLiftedGradientSpace.LiftTangent) => iteratedFDeriv ℝ n (F z.1) z.2) :

Continuous fun (z : K × EulerLiftedGradientSpace.LiftDomain P) => jetSeries P (F z.1) z.2 n

source

theorem EulerCylinderCoverDescent.descend_comp_map (P : ℝ) [Fact (0 < P)] {W : Type u_1} (f : EulerLiftedGradientSpace.LiftTangent → W) (hperiod : ∀ (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent), f (z.1, ↑c + z.2) = f z) (Φ : EulerLiftedGradientSpace.LiftTangent → EulerLiftedGradientSpace.LiftTangent) :

descend P (f ∘ Φ) = descend P f ∘ descendMap P Φ

source

theorem EulerCylinderCoverDescent.jetSeries_comp (P : ℝ) [Fact (0 < P)] {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (f : EulerLiftedGradientSpace.LiftTangent → W) (hperiod : ∀ (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent), f (z.1, ↑c + z.2) = f z) (Φ : EulerLiftedGradientSpace.LiftTangent → EulerLiftedGradientSpace.LiftTangent) (hf : ContDiff ℝ (↑⊤) f) (hΦ : ContDiff ℝ (↑⊤) Φ) (q : EulerLiftedGradientSpace.LiftDomain P) (n : ℕ) :

jetSeries P (f ∘ Φ) q n = (jetSeries P f (descendMap P Φ q)).taylorComp (jetSeries P Φ q) n

source

theorem EulerCylinderCoverDescent.comp_deck (P : ℝ) {W : Type u_1} (f : EulerLiftedGradientSpace.LiftTangent → W) (hperiod : ∀ (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent), f (z.1, ↑c + z.2) = f z) (Φ : EulerLiftedGradientSpace.LiftTangent → EulerLiftedGradientSpace.LiftTangent) (hΦ : ∀ (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent), Φ (z.1, ↑c + z.2) = ((Φ z).1, ↑c + (Φ z).2)) (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent) :

(f ∘ Φ) (z.1, ↑c + z.2) = (f ∘ Φ) z

source

theorem EulerCylinderCoverDescent.local_jet_comp (P : ℝ) [Fact (0 < P)] {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (f : EulerLiftedGradientSpace.LiftTangent → W) (hperiod : ∀ (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent), f (z.1, ↑c + z.2) = f z) (Φ : EulerLiftedGradientSpace.LiftTangent → EulerLiftedGradientSpace.LiftTangent) (hdeck : ∀ (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent), Φ (z.1, ↑c + z.2) = ((Φ z).1, ↑c + (Φ z).2)) (hf : ContDiff ℝ (↑⊤) f) (hΦ : ContDiff ℝ (↑⊤) Φ) (q : EulerLiftedGradientSpace.LiftDomain P) (n : ℕ) :

iteratedFDeriv ℝ n (EulerMetricTransport.localFieldLift P (descend P f ∘ descendMap P Φ) q) 0 = (jetSeries P f (descendMap P Φ q)).taylorComp (jetSeries P Φ q) n