Genuine smooth L² sums, scalar products, and ordinary advection.

def EulerOrdinarySobolev.sumField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {ι : Type u_2} (I : Finset ι) (A : ι → EulerLpTranslation.SmoothL2Field V) : EulerLpTranslation.SmoothL2Field V

Sum field, bundling field, smooth, integrable, have and the required compatibility proofs.

Equations

• EulerOrdinarySobolev.sumField I A = { field := fun (x : EulerSmoothLimit.Space) => ∑ i ∈ I, (A i).field x, smooth := ⋯, integrable := ⋯ }

@[simp]

theorem EulerOrdinarySobolev.sumField_field {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {ι : Type u_2} (I : Finset ι) (A : ι → EulerLpTranslation.SmoothL2Field V) (x : EulerSmoothLimit.Space) : (sumField I A).field x = ∑ i ∈ I, (A i).field x

theorem EulerOrdinarySobolev.toLp_sumField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {ι : Type u_2} (I : Finset ι) (A : ι → EulerLpTranslation.SmoothL2Field V) : (sumField I A).toLp = ∑ i ∈ I, (A i).toLp

theorem EulerOrdinarySobolev.wordField_sum {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {ι : Type u_2} (I : Finset ι) (A : ι → EulerLpTranslation.SmoothL2Field V) {n : ℕ} (w : Fin n → Fin 3) : wordField (sumField I A) w = sumField I fun (i : ι) => wordField (A i) w

def EulerOrdinarySobolev.fieldNeg {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : EulerLpTranslation.SmoothL2Field V) : EulerLpTranslation.SmoothL2Field V

Field neg, given by mapField (-(ContinuousLinearMap.id ℝ V)) A.

Equations

• EulerOrdinarySobolev.fieldNeg A = EulerLpTranslation.SmoothL2Field.mapField (-ContinuousLinearMap.id ℝ V) A

@[simp]

theorem EulerOrdinarySobolev.fieldNeg_field {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : EulerLpTranslation.SmoothL2Field V) (x : EulerSmoothLimit.Space) : (fieldNeg A).field x = -A.field x

def EulerOrdinarySobolev.fieldSub {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A B : EulerLpTranslation.SmoothL2Field V) : EulerLpTranslation.SmoothL2Field V

Field sub, given by addField A (fieldNeg B).

Equations

• EulerOrdinarySobolev.fieldSub A B = A.addField (EulerOrdinarySobolev.fieldNeg B)

@[simp]

theorem EulerOrdinarySobolev.fieldSub_field {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A B : EulerLpTranslation.SmoothL2Field V) (x : EulerSmoothLimit.Space) : (fieldSub A B).field x = A.field x - B.field x

theorem EulerOrdinarySobolev.toLp_fieldNeg {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : EulerLpTranslation.SmoothL2Field V) : (fieldNeg A).toLp = -A.toLp

theorem EulerOrdinarySobolev.toLp_fieldSub {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A B : EulerLpTranslation.SmoothL2Field V) : (fieldSub A B).toLp = A.toLp - B.toLp

noncomputable def EulerOrdinarySobolev.scalarProduct {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : EulerLpTranslation.SmoothL2Field ℝ) (B : EulerLpTranslation.SmoothL2Field V) : EulerLpTranslation.SmoothL2Field V

Scalar product, constructed using product.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem EulerOrdinarySobolev.scalarProduct_field {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : EulerLpTranslation.SmoothL2Field ℝ) (B : EulerLpTranslation.SmoothL2Field V) (x : EulerSmoothLimit.Space) : (scalarProduct A B).field x = A.field x • B.field x

theorem EulerOrdinarySobolev.scalarProduct_directional {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : EulerLpTranslation.SmoothL2Field ℝ) (B : EulerLpTranslation.SmoothL2Field V) (v : EulerSmoothLimit.Space) : (scalarProduct A B).directionalField v = (scalarProduct (A.directionalField v) B).addField (scalarProduct A (B.directionalField v))

theorem EulerOrdinarySobolev.scalarProduct_norm_left {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : EulerLpTranslation.SmoothL2Field ℝ) (B : EulerLpTranslation.SmoothL2Field V) (M : ℝ) (hM : ∀ (x : EulerSmoothLimit.Space), ‖A.field x‖ ≤ M) : ‖(scalarProduct A B).toLp‖ ≤ M * ‖B.toLp‖

theorem EulerOrdinarySobolev.scalarProduct_norm_right {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : EulerLpTranslation.SmoothL2Field ℝ) (B : EulerLpTranslation.SmoothL2Field V) (M : ℝ) (hM : ∀ (x : EulerSmoothLimit.Space), ‖B.field x‖ ≤ M) : ‖(scalarProduct A B).toLp‖ ≤ M * ‖A.toLp‖

noncomputable def EulerOrdinarySobolev.coordinateProduct {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (i : Fin 3) (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (B : EulerLpTranslation.SmoothL2Field V) : EulerLpTranslation.SmoothL2Field V

Coordinate product, given by scalarProduct (mapField (EuclideanSpace.proj i) A) B.

Equations

• EulerOrdinarySobolev.coordinateProduct i A B = EulerOrdinarySobolev.scalarProduct (EulerLpTranslation.SmoothL2Field.mapField (EuclideanSpace.proj i) A) B

@[simp]

theorem EulerOrdinarySobolev.coordinateProduct_field {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (i : Fin 3) (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (B : EulerLpTranslation.SmoothL2Field V) (x : EulerSmoothLimit.Space) : (coordinateProduct i A B).field x = (A.field x).ofLp i • B.field x

noncomputable def EulerOrdinarySobolev.advectionField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (B : EulerLpTranslation.SmoothL2Field V) : EulerLpTranslation.SmoothL2Field V

Advection field, given by sumField univ (fun i : Fin 3 => coordinateProduct i A (B.directionalField (axis i))).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem EulerOrdinarySobolev.advectionField_field {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (B : EulerLpTranslation.SmoothL2Field V) (x : EulerSmoothLimit.Space) : (advectionField A B).field x = (fderiv ℝ B.field x) (A.field x)