Interior products of rough differential forms

Insertion of a vector field into the first slot lowers the degree of a bundle-valued form by one and squares to zero without further continuity assumptions on the coefficient fibres. Additivity in the field and the form requires ContinuousAdd on each fibre, scalar laws require ContinuousConstSMul ℝ, and anticommutation requires IsTopologicalAddGroup. Pullback commutes with insertion of related fields, also within arbitrary sets. These operations provide the algebraic input for Cartan's calculus and contraction of volume forms. We use Mathlib's AlternatingMap.curryLeft and retain continuity of the remaining variables. This works for arbitrary topological coefficient fibres without choosing fibre norms. For fixed normed coefficients on the model space it agrees with ContinuousAlternatingMap.curryLeft, and in the chart at a point it is curryLeft of the coordinate expressions of the form and the field. Consequently the interior product of a differentiable field and a differentiable form is a differentiable form, and that of a C^n field and a C^n form is a C^n form.

References

• John M. Lee, Introduction to Smooth Manifolds, second edition, Chapter 14.

noncomputable def TauCeti.bundleInterior {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {V : M → Type u_4} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] {k : ℕ} (X : (x : M) → TangentSpace I x) (ω : RoughBundleForm I M V (k + 1)) : RoughBundleForm I M V k

Insert a vector field into the first slot of a rough bundle-valued form. The value bundle is unchanged, and no regularity of the field or the form in the base point is required.

@[simp]

theorem TauCeti.bundleInterior_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {V : M → Type u_4} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] {k : ℕ} (X : (x : M) → TangentSpace I x) (ω : RoughBundleForm I M V (k + 1)) (x : M) (v : Fin k → TangentSpace I x) : (bundleInterior X ω x) v = (ω x) (Matrix.vecCons (X x) v)

Interior product is insertion into the first slot.

theorem TauCeti.bundleInterior_apply_eq_curryLeftTopological {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {V : M → Type u_4} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] {k : ℕ} [∀ (x : M), ContinuousAdd (V x)] [∀ (x : M), ContinuousConstSMul ℝ (V x)] (X : (x : M) → TangentSpace I x) (ω : RoughBundleForm I M V (k + 1)) (x : M) : bundleInterior X ω x = (ω x).curryLeftTopological (X x)

At a point, insertion is the topological continuous currying operation.

@[simp]

theorem TauCeti.bundleInterior_zero_field {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {V : M → Type u_4} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] {k : ℕ} (ω : RoughBundleForm I M V (k + 1)) : bundleInterior 0 ω = 0

Insertion of the zero field vanishes.

@[simp]

theorem TauCeti.bundleInterior_zero {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {V : M → Type u_4} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] {k : ℕ} (X : (x : M) → TangentSpace I x) : bundleInterior X 0 = 0

Insertion into the zero form vanishes.

@[simp]

theorem TauCeti.bundleInterior_add_field {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {V : M → Type u_4} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] {k : ℕ} [∀ (x : M), ContinuousAdd (V x)] (X Y : (x : M) → TangentSpace I x) (ω : RoughBundleForm I M V (k + 1)) : bundleInterior (X + Y) ω = bundleInterior X ω + bundleInterior Y ω

Interior product is additive in the vector field.

@[simp]

theorem TauCeti.bundleInterior_smul_field {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {V : M → Type u_4} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] {k : ℕ} [∀ (x : M), ContinuousConstSMul ℝ (V x)] (a : M → ℝ) (X : (x : M) → TangentSpace I x) (ω : RoughBundleForm I M V (k + 1)) : bundleInterior (fun (x : M) => a x • X x) ω = fun (x : M) => a x • bundleInterior X ω x

Interior product respects pointwise scalar multiplication of the vector field.

@[simp]

theorem TauCeti.bundleInterior_add {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {V : M → Type u_4} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] {k : ℕ} [∀ (x : M), ContinuousAdd (V x)] (X : (x : M) → TangentSpace I x) (ω η : RoughBundleForm I M V (k + 1)) : bundleInterior X (ω + η) = bundleInterior X ω + bundleInterior X η

Interior product is additive in the form.

@[simp]

theorem TauCeti.bundleInterior_smul {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {V : M → Type u_4} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] {k : ℕ} [∀ (x : M), ContinuousConstSMul ℝ (V x)] (a : M → ℝ) (X : (x : M) → TangentSpace I x) (ω : RoughBundleForm I M V (k + 1)) : (bundleInterior X fun (x : M) => a x • ω x) = fun (x : M) => a x • bundleInterior X ω x

Interior product respects pointwise scalar multiplication of the form.

@[simp]

theorem TauCeti.bundleInterior_self {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {V : M → Type u_4} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] {k : ℕ} (X : (x : M) → TangentSpace I x) (ω : RoughBundleForm I M V (k + 2)) : bundleInterior X (bundleInterior X ω) = 0

Inserting the same field twice gives zero.

theorem TauCeti.bundleInterior_swap {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {V : M → Type u_4} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] {k : ℕ} [∀ (x : M), IsTopologicalAddGroup (V x)] (X Y : (x : M) → TangentSpace I x) (ω : RoughBundleForm I M V (k + 2)) : bundleInterior X (bundleInterior Y ω) = -bundleInterior Y (bundleInterior X ω)

Interior products by two vector fields anticommute.

theorem TauCeti.bundleMpullbackWithin_interior_at {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k : ℕ} {E' : Type u_5} {H' : Type u_6} {M' : Type u_7} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {W : M' → Type u_8} [(y : M') → AddCommGroup (W y)] [(y : M') → Module ℝ (W y)] [(y : M') → TopologicalSpace (W y)] (f : M → M') (s : Set M) (X : (x : M) → TangentSpace I x) (Y : (y : M') → TangentSpace I' y) (ω : RoughBundleForm I' M' W (k + 1)) {x : M} (hXY : (mfderiv[s] f x) (X x) = Y (f x)) : bundleMpullbackWithin I I' f s (bundleInterior Y ω) x = bundleInterior X (bundleMpullbackWithin I I' f s ω) x

Within-set pullback commutes with insertion of fields related by the within-set derivative at the specified point. No differentiability hypothesis is needed beyond this equality.

theorem TauCeti.bundleMpullback_interior_at {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k : ℕ} {E' : Type u_5} {H' : Type u_6} {M' : Type u_7} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {W : M' → Type u_8} [(y : M') → AddCommGroup (W y)] [(y : M') → Module ℝ (W y)] [(y : M') → TopologicalSpace (W y)] (f : M → M') (X : (x : M) → TangentSpace I x) (Y : (y : M') → TangentSpace I' y) (ω : RoughBundleForm I' M' W (k + 1)) {x : M} (hXY : (mfderiv% f x) (X x) = Y (f x)) : bundleMpullback I I' f (bundleInterior Y ω) x = bundleInterior X (bundleMpullback I I' f ω) x

Pullback commutes with insertion of fields related by the derivative at a point.

theorem TauCeti.bundleMpullbackWithin_interior {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k : ℕ} {E' : Type u_5} {H' : Type u_6} {M' : Type u_7} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {W : M' → Type u_8} [(y : M') → AddCommGroup (W y)] [(y : M') → Module ℝ (W y)] [(y : M') → TopologicalSpace (W y)] (f : M → M') (s : Set M) (X : (x : M) → TangentSpace I x) (Y : (y : M') → TangentSpace I' y) (ω : RoughBundleForm I' M' W (k + 1)) (hXY : ∀ (x : M), (mfderiv[s] f x) (X x) = Y (f x)) : bundleMpullbackWithin I I' f s (bundleInterior Y ω) = bundleInterior X (bundleMpullbackWithin I I' f s ω)

Within-set pullback commutes with interior products of related fields.

theorem TauCeti.bundleMpullback_interior {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k : ℕ} {E' : Type u_5} {H' : Type u_6} {M' : Type u_7} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {W : M' → Type u_8} [(y : M') → AddCommGroup (W y)] [(y : M') → Module ℝ (W y)] [(y : M') → TopologicalSpace (W y)] (f : M → M') (X : (x : M) → TangentSpace I x) (Y : (y : M') → TangentSpace I' y) (ω : RoughBundleForm I' M' W (k + 1)) (hXY : ∀ (x : M), (mfderiv% f x) (X x) = Y (f x)) : bundleMpullback I I' f (bundleInterior Y ω) = bundleInterior X (bundleMpullback I I' f ω)

Pullback commutes with interior products of related fields.

noncomputable def TauCeti.RoughForm.interior {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k : ℕ} {F : Type u_5} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (X : (x : M) → TangentSpace I x) (ω : RoughForm I M F (k + 1)) : RoughForm I M F k

The interior product of a vector field with a fixed-coefficient form.

theorem TauCeti.RoughForm.interior_def {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k : ℕ} {F : Type u_5} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (X : (x : M) → TangentSpace I x) (ω : RoughForm I M F (k + 1)) : interior X ω = bundleInterior X ω

The fixed-coefficient interior product is the corresponding bundle-valued insertion.

@[simp]

theorem TauCeti.RoughForm.interior_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k : ℕ} {F : Type u_5} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (X : (x : M) → TangentSpace I x) (ω : RoughForm I M F (k + 1)) (x : M) (v : Fin k → TangentSpace I x) : (interior X ω x) v = (ω x) (Matrix.vecCons (X x) v)

Evaluation of the interior product is insertion into the first slot.

@[simp]

theorem TauCeti.RoughForm.interior_zero_field {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k : ℕ} {F : Type u_5} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (ω : RoughForm I M F (k + 1)) : interior 0 ω = 0

Insertion of the zero field vanishes.

@[simp]

theorem TauCeti.RoughForm.interior_zero {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k : ℕ} {F : Type u_5} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (X : (x : M) → TangentSpace I x) : interior X 0 = 0

The interior product of the zero form vanishes.

@[simp]

theorem TauCeti.RoughForm.interior_add_field {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k : ℕ} {F : Type u_5} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousAdd F] (X Y : (x : M) → TangentSpace I x) (ω : RoughForm I M F (k + 1)) : interior (X + Y) ω = interior X ω + interior Y ω

Interior product is additive in the vector field.

@[simp]

theorem TauCeti.RoughForm.interior_smul_field {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k : ℕ} {F : Type u_5} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousConstSMul ℝ F] (a : M → ℝ) (X : (x : M) → TangentSpace I x) (ω : RoughForm I M F (k + 1)) : interior (fun (x : M) => a x • X x) ω = fun (x : M) => a x • interior X ω x

Interior product respects pointwise scalar multiplication of the vector field.

@[simp]

theorem TauCeti.RoughForm.interior_add {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k : ℕ} {F : Type u_5} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousAdd F] (X : (x : M) → TangentSpace I x) (ω η : RoughForm I M F (k + 1)) : interior X (ω + η) = interior X ω + interior X η

Interior product distributes over addition of forms.

@[simp]

theorem TauCeti.RoughForm.interior_smul_pointwise {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k : ℕ} {F : Type u_5} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousConstSMul ℝ F] (a : M → ℝ) (X : (x : M) → TangentSpace I x) (ω : RoughForm I M F (k + 1)) : (interior X fun (x : M) => a x • ω x) = fun (x : M) => a x • interior X ω x

Interior product respects pointwise scalar multiplication of the form.

@[simp]

theorem TauCeti.RoughForm.interior_smul {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k : ℕ} {F : Type u_5} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousConstSMul ℝ F] (c : ℝ) (X : (x : M) → TangentSpace I x) (ω : RoughForm I M F (k + 1)) : interior X (c • ω) = c • interior X ω

Interior product commutes with constant scalar multiplication of forms.

@[simp]

theorem TauCeti.RoughForm.interior_self {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k : ℕ} {F : Type u_5} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (X : (x : M) → TangentSpace I x) (ω : RoughForm I M F (k + 2)) : interior X (interior X ω) = 0

Inserting the same field twice gives zero.

theorem TauCeti.RoughForm.interior_eq_zero_of_interior_eq {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k : ℕ} {F : Type u_5} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {ω : RoughForm I M F (k + 2)} {α : RoughForm I M F (k + 1)} {X : (x : M) → TangentSpace I x} (h : interior X ω = α) : interior X α = 0

A form vanishes on a field into which it was obtained by insertion: if ι_X ω = α, then ι_X α = ω(X, X, ...) = 0. For a one-form α and ω = dα this says that a primitive vanishes on its Liouville field.

theorem TauCeti.RoughForm.apply_eq_zero_of_interior_eq {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {F : Type u_5} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {ω : RoughForm I M F 2} {α : RoughForm I M F 1} {X : (x : M) → TangentSpace I x} (h : interior X ω = α) (y : M) : (α y) ![X y] = 0

Pointwise form of RoughForm.interior_eq_zero_of_interior_eq for one-forms: if ι_X ω = α for a two-form ω, then α_y(X_y) = 0 at every point y.

theorem TauCeti.RoughForm.interior_swap {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k : ℕ} {F : Type u_5} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup F] (X Y : (x : M) → TangentSpace I x) (ω : RoughForm I M F (k + 2)) : interior X (interior Y ω) = -interior Y (interior X ω)

Interior products by two vector fields anticommute.

theorem TauCeti.mpullbackWithin_interior_at {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k : ℕ} {F : Type u_5} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {E' : Type u_6} {H' : Type u_7} {M' : Type u_8} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} (f : M → M') (s : Set M) (X : (x : M) → TangentSpace I x) (Y : (y : M') → TangentSpace I' y) (ω : RoughForm I' M' F (k + 1)) {x : M} (hXY : (mfderiv[s] f x) (X x) = Y (f x)) : mpullbackWithin I I' f s (RoughForm.interior Y ω) x = RoughForm.interior X (mpullbackWithin I I' f s ω) x

Within-set pullback of a fixed-coefficient interior product, for fields related at a point.

theorem TauCeti.mpullback_interior_at {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k : ℕ} {F : Type u_5} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {E' : Type u_6} {H' : Type u_7} {M' : Type u_8} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} (f : M → M') (X : (x : M) → TangentSpace I x) (Y : (y : M') → TangentSpace I' y) (ω : RoughForm I' M' F (k + 1)) {x : M} (hXY : (mfderiv% f x) (X x) = Y (f x)) : mpullback I I' f (RoughForm.interior Y ω) x = RoughForm.interior X (mpullback I I' f ω) x

Pullback of a fixed-coefficient interior product, for fields related at a point.

theorem TauCeti.mpullbackWithin_interior {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k : ℕ} {F : Type u_5} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {E' : Type u_6} {H' : Type u_7} {M' : Type u_8} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} (f : M → M') (s : Set M) (X : (x : M) → TangentSpace I x) (Y : (y : M') → TangentSpace I' y) (ω : RoughForm I' M' F (k + 1)) (hXY : ∀ (x : M), (mfderiv[s] f x) (X x) = Y (f x)) : mpullbackWithin I I' f s (RoughForm.interior Y ω) = RoughForm.interior X (mpullbackWithin I I' f s ω)

Within-set pullback of a fixed-coefficient interior product, for related fields.

theorem TauCeti.mpullback_interior {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k : ℕ} {F : Type u_5} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {E' : Type u_6} {H' : Type u_7} {M' : Type u_8} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} (f : M → M') (X : (x : M) → TangentSpace I x) (Y : (y : M') → TangentSpace I' y) (ω : RoughForm I' M' F (k + 1)) (hXY : ∀ (x : M), (mfderiv% f x) (X x) = Y (f x)) : mpullback I I' f (RoughForm.interior Y ω) = RoughForm.interior X (mpullback I I' f ω)

Pullback of a fixed-coefficient interior product, for related fields.

theorem TauCeti.RoughForm.interior_apply_eq_curryLeft {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k : ℕ} {F : Type u_6} [NormedAddCommGroup F] [NormedSpace ℝ F] (X : (x : M) → TangentSpace I x) (ω : RoughForm I M F (k + 1)) (x : M) : interior X ω x = (ω x).curryLeft (X x)

For normed coefficients, the interior product at a point is Mathlib's continuous currying operation applied to the value of the form.

theorem TauCeti.RoughForm.interior_modelSpace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {k : ℕ} {F : Type u_6} [NormedAddCommGroup F] [NormedSpace ℝ F] (X : E → E) (ω : RoughForm (modelWithCornersSelf ℝ E) E F (k + 1)) : interior X ω = fun (x : E) => (ω x).curryLeft (X x)

On the model space, the interior product is Mathlib's continuous currying operation.

theorem TauCeti.RoughForm.inChartAt_interior {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k : ℕ} {F : Type u_6} [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] (X : (x : M) → TangentSpace I x) (ω : RoughForm I M F (k + 1)) {x : M} {z : E} (hz : z ∈ (extChartAt I x).target) : (interior X ω).inChartAt x z = (ω.inChartAt x z).curryLeft (VectorField.mpullbackWithin (modelWithCornersSelf ℝ E) I (↑(extChartAt I x).symm) X (Set.range ↑I) z)

In the chart at x, the interior product of a form with a vector field is the interior product of the coordinate expressions of the form and of the field.

theorem TauCeti.RoughForm.mdifferentiableAt_interior {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k : ℕ} {F : Type u_6} [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {X : (x : M) → TangentSpace I x} {ω : RoughForm I M F (k + 1)} {x : M} (hX : (MDiffAt fun (y : M) => ⟨y, X y⟩) x) (hω : (MDiffAt fun (y : M) => ⟨y, ω y⟩) x) : (MDiffAt fun (y : M) => ⟨y, interior X ω y⟩) x

The interior product of a vector field and a fixed-coefficient form, both differentiable at a point, is a section of the alternating bundle differentiable at that point.

theorem TauCeti.RoughForm.contMDiffAt_interior {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k : ℕ} {F : Type u_6} [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {n : WithTop ℕ∞} {X : (x : M) → TangentSpace I x} {ω : RoughForm I M F (k + 1)} {x : M} (hX : ContMDiffAt I I.tangent n (fun (y : M) => ⟨y, X y⟩) x) (hω : ContMDiffAt I (I.prod (modelWithCornersSelf ℝ (E [⋀^Fin (k + 1)]→L[ℝ] F))) n (fun (y : M) => ⟨y, ω y⟩) x) : ContMDiffAt I (I.prod (modelWithCornersSelf ℝ (E [⋀^Fin k]→L[ℝ] F))) n (fun (y : M) => ⟨y, interior X ω y⟩) x

The interior product of a vector field and a fixed-coefficient form, both C^n at a point, is a section of the alternating bundle which is C^n at that point.

theorem TauCeti.IsSmoothForm.interior {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k : ℕ} {F : Type u_6} [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {n : WithTop ℕ∞} {X : (x : M) → TangentSpace I x} {ω : RoughForm I M F (k + 1)} (hω : IsSmoothForm I n ω) (hX : ContMDiff I I.tangent n fun (y : M) => ⟨y, X y⟩) : IsSmoothForm I n (RoughForm.interior X ω)

The interior product of a C^n vector field and a C^n fixed-coefficient form is a C^n form.