Reconstructing actual L² tensors from finitely many coordinate fields

This qualitative finite-dimensional construction supplies literal tensor-valued L² derivatives. Quantitative Gevrey estimates continue to use the ordered-word norms directly, and do not pass through these coordinate norm equivalences.

noncomputable def EulerLpFiniteTensor.tupleLp {X : Type u_1} {V : Type u_2} [MeasurableSpace X] [NormedAddCommGroup V] [NormedSpace ℝ V] (μ : MeasureTheory.Measure X) {ι : Type u_3} [Fintype ι] : (ι → ↥(MeasureTheory.Lp V 2 μ)) →L[ℝ] ↥(MeasureTheory.Lp (ι → V) 2 μ)

A finite tuple of L² classes gives its literal product-valued L² class.

Equations

• EulerLpFiniteTensor.tupleLp μ = ∑ i : ι, ContinuousLinearMap.compLpL 2 μ (ContinuousLinearMap.single ℝ (fun (x : ι) => V) i) ∘SL ContinuousLinearMap.proj i

theorem EulerLpFiniteTensor.tupleLp_ae {X : Type u_1} {V : Type u_2} [MeasurableSpace X] [NormedAddCommGroup V] [NormedSpace ℝ V] (μ : MeasureTheory.Measure X) {ι : Type u_3} [Fintype ι] (u : ι → ↥(MeasureTheory.Lp V 2 μ)) : ↑↑((tupleLp μ) u) =ᵐ[μ] fun (x : X) (i : ι) => ↑↑(u i) x

noncomputable def EulerLpFiniteTensor.direction (i : Fin 3) : EulerSmoothLimit.Space

Coordinate directions in the ordinary spatial domain.

Equations

• EulerLpFiniteTensor.direction i = EuclideanSpace.single i 1

noncomputable def EulerLpFiniteTensor.tensorCoordinates {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] (n : ℕ) : (EulerSmoothLimit.Space [×n]→L[ℝ] V) →L[ℝ] (Fin n → Fin 3) → V

Tensor coordinates, given by ContinuousLinearMap.pi (fun w => (ContinuousLinearMap.id ℝ (Space [×n]→L[ℝ] V)).flipMultilinear (fun i => direction (w i))).

Equations

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

@[simp]

theorem EulerLpFiniteTensor.tensorCoordinates_apply {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] (n : ℕ) (A : EulerSmoothLimit.Space [×n]→L[ℝ] V) (w : Fin n → Fin 3) : (tensorCoordinates n) A w = A fun (i : Fin n) => direction (w i)

theorem EulerLpFiniteTensor.tensorCoordinates_injective {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] (n : ℕ) : Function.Injective ⇑(tensorCoordinates n)

noncomputable def EulerLpFiniteTensor.tensorReassembly {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (n : ℕ) : ((Fin n → Fin 3) → V) →L[ℝ] EulerSmoothLimit.Space [×n]→L[ℝ] V

A fixed bounded left inverse of the finite coordinate evaluation map.

Equations

• EulerLpFiniteTensor.tensorReassembly n = LinearMap.toContinuousLinearMap (↑(EulerLpFiniteTensor.tensorCoordinates n)).leftInverse

@[simp]

theorem EulerLpFiniteTensor.tensorReassembly_coordinates {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (n : ℕ) (A : EulerSmoothLimit.Space [×n]→L[ℝ] V) : (tensorReassembly n) ((tensorCoordinates n) A) = A

noncomputable def EulerLpFiniteTensor.tensorLpReassembly {X : Type u_1} {V : Type u_2} [MeasurableSpace X] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (μ : MeasureTheory.Measure X) (n : ℕ) : ((Fin n → Fin 3) → ↥(MeasureTheory.Lp V 2 μ)) →L[ℝ] ↥(MeasureTheory.Lp (EulerSmoothLimit.Space [×n]→L[ℝ] V) 2 μ)

Reconstruction is a genuine bounded map on the finite tuple of L² classes.

Equations

• EulerLpFiniteTensor.tensorLpReassembly μ n = ContinuousLinearMap.compLpL 2 μ (EulerLpFiniteTensor.tensorReassembly n) ∘SL EulerLpFiniteTensor.tupleLp μ

theorem EulerLpFiniteTensor.tensorLpReassembly_ae {X : Type u_1} {V : Type u_2} [MeasurableSpace X] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (μ : MeasureTheory.Measure X) (n : ℕ) (u : (Fin n → Fin 3) → ↥(MeasureTheory.Lp V 2 μ)) : ↑↑((tensorLpReassembly μ n) u) =ᵐ[μ] fun (x : X) => (tensorReassembly n) fun (w : Fin n → Fin 3) => ↑↑(u w) x

theorem EulerLpFiniteTensor.tensorLpReassembly_eq_ae {X : Type u_1} {V : Type u_2} [MeasurableSpace X] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (μ : MeasureTheory.Measure X) (n : ℕ) (u : (Fin n → Fin 3) → ↥(MeasureTheory.Lp V 2 μ)) (f : X → EulerSmoothLimit.Space [×n]→L[ℝ] V) (h : ∀ (w : Fin n → Fin 3), ↑↑(u w) =ᵐ[μ] fun (x : X) => (f x) fun (i : Fin n) => direction (w i)) : ↑↑((tensorLpReassembly μ n) u) =ᵐ[μ] f

If the coordinate L² classes represent a literal tensor field, their reconstruction represents that field, with no integrability assumption on it.