A series of genuine smooth spatial L² fields that is absolutely summable at every finite Sobolev order has one smooth L² sum.

theorem EulerSmoothL2Series.instSmoothL2Series1 : Fact (0 < 1)

theorem EulerSmoothL2Series.tensorNorm_eq_derivativeSum (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (s : ℕ) : EulerOrdinarySobolev.tensorNorm s A = EulerPhysicalL2Scaling.derivativeSum s A.field

theorem EulerSmoothL2Series.tensorNorm_add_le (A B : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (s : ℕ) : EulerOrdinarySobolev.tensorNorm s (A.addField B) ≤ EulerOrdinarySobolev.tensorNorm s A + EulerOrdinarySobolev.tensorNorm s B

theorem EulerSmoothL2Series.zeroField_jet (n : ℕ) : EulerLpTranslation.SmoothL2Field.zeroField.jetLp n = 0

theorem EulerSmoothL2Series.zeroField_value : EulerLpTranslation.SmoothL2Field.zeroField.toLp = 0

def EulerSmoothL2Series.partialSum (A : ℕ → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : ℕ → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Partial sum as an element of ℕ → SmoothL2Field Space | 0 => zeroField | n+1 => addField (partialSum A n) (A n).

Equations

• EulerSmoothL2Series.partialSum A 0 = EulerLpTranslation.SmoothL2Field.zeroField
• EulerSmoothL2Series.partialSum A n.succ = (EulerSmoothL2Series.partialSum A n).addField (A n)

theorem EulerSmoothL2Series.partialSum_field (A : ℕ → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (n : ℕ) (x : EulerSmoothLimit.Space) : (partialSum A n).field x = ∑ i ∈ Finset.range n, (A i).field x

theorem EulerSmoothL2Series.partialSum_jet (A : ℕ → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (n q : ℕ) : (partialSum A n).jetLp q = ∑ i ∈ Finset.range n, (A i).jetLp q

theorem EulerSmoothL2Series.partialSum_value (A : ℕ → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (n : ℕ) : (partialSum A n).toLp = ∑ i ∈ Finset.range n, (A i).toLp

theorem EulerSmoothL2Series.partialSum_norm (A : ℕ → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (n q : ℕ) : EulerOrdinarySobolev.tensorNorm q (partialSum A n) ≤ ∑ i ∈ Finset.range n, EulerOrdinarySobolev.tensorNorm q (A i)

theorem EulerSmoothL2Series.tensorNorm_zero (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : EulerOrdinarySobolev.tensorNorm 0 A = ‖A.toLp‖

theorem EulerSmoothL2Series.partialSum_uniform_bound (A : ℕ → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (q : ℕ), Summable fun (n : ℕ) => EulerOrdinarySobolev.tensorNorm q (A n)) (n q : ℕ) : EulerOrdinarySobolev.tensorNorm q (partialSum A n) ≤ ∑' (i : ℕ), EulerOrdinarySobolev.tensorNorm q (A i)

theorem EulerSmoothL2Series.partialSum_value_cauchy (A : ℕ → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (q : ℕ), Summable fun (n : ℕ) => EulerOrdinarySobolev.tensorNorm q (A n)) : CauchySeq fun (n : ℕ) => (partialSum A n).toLp

theorem EulerSmoothL2Series.partialSum_path_cauchy (A : ℕ → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (q : ℕ), Summable fun (n : ℕ) => EulerOrdinarySobolev.tensorNorm q (A n)) : CauchySeq fun (n : ℕ) => EulerOrdinarySobolev.fieldPath (fun (x : ↑(Set.Icc 0 0)) => partialSum A n) ⋯

noncomputable def EulerSmoothL2Series.limitData (A : ℕ → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (q : ℕ), Summable fun (n : ℕ) => EulerOrdinarySobolev.tensorNorm q (A n)) : EulerOrdinarySobolev.SmoothLimitData (fun (n : ℕ) (x : ↑(Set.Icc 0 0)) => partialSum A n) ⋯

Limit data, constructed using smoothLimitData.

Equations

• EulerSmoothL2Series.limitData A hA = EulerOrdinarySobolev.smoothLimitData EulerSmoothL2Series.limitData._proof_1 (fun (n : ℕ) (x : ↑(Set.Icc 0 0)) => EulerSmoothL2Series.partialSum A n) ⋯ ⋯ ⋯

noncomputable def EulerSmoothL2Series.sumField (A : ℕ → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (q : ℕ), Summable fun (n : ℕ) => EulerOrdinarySobolev.tensorNorm q (A n)) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Sum field, given by (limitData A hA).field ⟨0,le_rfl,le_rfl⟩.

Equations

• EulerSmoothL2Series.sumField A hA = (EulerSmoothL2Series.limitData A hA).field ⟨0, EulerSmoothL2Series.sumField._proof_1⟩

theorem EulerSmoothL2Series.sumField_jet_tendsto (A : ℕ → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (q : ℕ), Summable fun (n : ℕ) => EulerOrdinarySobolev.tensorNorm q (A n)) (q : ℕ) : Filter.Tendsto (fun (n : ℕ) => (partialSum A n).jetLp q) Filter.atTop (nhds ((sumField A hA).jetLp q))

theorem EulerSmoothL2Series.sumField_value_tendsto (A : ℕ → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (q : ℕ), Summable fun (n : ℕ) => EulerOrdinarySobolev.tensorNorm q (A n)) : Filter.Tendsto (fun (n : ℕ) => (partialSum A n).toLp) Filter.atTop (nhds (sumField A hA).toLp)

theorem EulerSmoothL2Series.sumField_Hm_tendsto (A : ℕ → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (q : ℕ), Summable fun (n : ℕ) => EulerOrdinarySobolev.tensorNorm q (A n)) (q : ℕ) : Filter.Tendsto (fun (n : ℕ) => ∑ j ∈ Finset.range (q + 1), ‖(partialSum A n).jetLp j - (sumField A hA).jetLp j‖) Filter.atTop (nhds 0)

theorem EulerSmoothL2Series.sumField_derivativeSum_tendsto (A : ℕ → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (q : ℕ), Summable fun (n : ℕ) => EulerOrdinarySobolev.tensorNorm q (A n)) (q : ℕ) : Filter.Tendsto (fun (n : ℕ) => EulerPhysicalL2Scaling.derivativeSum q ((partialSum A n).field - (sumField A hA).field)) Filter.atTop (nhds 0)

theorem EulerSmoothL2Series.sumField_sobolev_tendsto (A : ℕ → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (q : ℕ), Summable fun (n : ℕ) => EulerOrdinarySobolev.tensorNorm q (A n)) (q : ℕ) : Filter.Tendsto (fun (n : ℕ) => EulerMeanSmoothRepresentative.ordinarySobolev q (partialSum A n).toLp ⋯) Filter.atTop (nhds (EulerMeanSmoothRepresentative.ordinarySobolev q (sumField A hA).toLp ⋯))

theorem EulerSmoothL2Series.sumField_pointwise_tendsto (A : ℕ → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (q : ℕ), Summable fun (n : ℕ) => EulerOrdinarySobolev.tensorNorm q (A n)) (x : EulerSmoothLimit.Space) : Filter.Tendsto (fun (n : ℕ) => (partialSum A n).field x) Filter.atTop (nhds ((sumField A hA).field x))

theorem EulerSmoothL2Series.sumField_support (A : ℕ → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (q : ℕ), Summable fun (n : ℕ) => EulerOrdinarySobolev.tensorNorm q (A n)) (S : Set EulerSmoothLimit.Space) (hS : IsClosed S) (hs : ∀ (n : ℕ), tsupport (A n).field ⊆ S) : tsupport (sumField A hA).field ⊆ S