Finite coordinate estimates for the physical tensor L2 norm.
theorem
AVenhance.Infra.Section4.amnr_pi_L2_le_sum
{ι : Type u_1}
[Fintype ι]
{F : Type u_2}
[NormedAddCommGroup F]
{μ : MeasureTheory.Measure AmnrSpace}
{f : AmnrSpace → ι → F}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
Coordinate L2 bounds control the actual finite Pi norm. This is the finite-dimensional bridge needed after the scalar contraction induction.
theorem
AVenhance.Infra.Section4.amnr_pi_L2_le_card
{ι : Type u_1}
[Fintype ι]
{F : Type u_2}
[NormedAddCommGroup F]
{μ : MeasureTheory.Measure AmnrSpace}
{f : AmnrSpace → ι → F}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
{B : ℝ}
(hb : ∀ (i : ι), MeasureTheory.eLpNorm (fun (z : AmnrSpace) => f z i) 2 μ ≤ ENNReal.ofReal B)
:
A uniform coordinate estimate controls the finite Pi norm with only the number of coordinates.
theorem
AVenhance.Infra.Section4.amnr_tensor_L2_le_eight
{μ : MeasureTheory.Measure AmnrSpace}
{A : AmnrSpace → Fin 2 → Fin 2 → Fin 2 → ℝ}
(hA : MeasureTheory.AEStronglyMeasurable A μ)
{B : ℝ}
(hb : ∀ (i j k : Fin 2), MeasureTheory.eLpNorm (fun (z : AmnrSpace) => A z i j k) 2 μ ≤ ENNReal.ofReal B)
:
The physical three-index tensor norm follows from its eight scalar coordinate estimates. This factor is uniform in every derivative index.