Local energies of actual L² fields, including the decomposition estimate.

noncomputable def EulerMeanHarmonic.localL2Energy (s : Set EulerSmoothLimit.Space) (u : ↥EulerMeanSolenoidal.L2) : ℝ

Local L² energy, given by ∫ x in s, ‖u x‖ ^ 2.

Equations

• EulerMeanHarmonic.localL2Energy s u = ∫ (x : EulerSmoothLimit.Space) in s, ‖↑↑u x‖ ^ 2

theorem EulerMeanHarmonic.lpNorm_coe_L2 (u : ↥EulerMeanSolenoidal.L2) : MeasureTheory.lpNorm (↑↑u) 2 MeasureTheory.volume = ‖u‖

theorem EulerMeanHarmonic.integrable_norm_sq_L2 (u : ↥EulerMeanSolenoidal.L2) : MeasureTheory.Integrable (fun (x : EulerSmoothLimit.Space) => ‖↑↑u x‖ ^ 2) MeasureTheory.volume

theorem EulerMeanHarmonic.integral_norm_sq_L2 (u : ↥EulerMeanSolenoidal.L2) : ∫ (x : EulerSmoothLimit.Space), ‖↑↑u x‖ ^ 2 = ‖u‖ ^ 2

theorem EulerMeanHarmonic.localL2Energy_nonneg (s : Set EulerSmoothLimit.Space) (u : ↥EulerMeanSolenoidal.L2) : 0 ≤ localL2Energy s u

theorem EulerMeanHarmonic.localL2Energy_le (s : Set EulerSmoothLimit.Space) (u : ↥EulerMeanSolenoidal.L2) : localL2Energy s u ≤ ‖u‖ ^ 2

theorem EulerMeanHarmonic.norm_add_sq_le_twice (a b : EulerSmoothLimit.Space) : ‖a + b‖ ^ 2 ≤ 2 * ‖a‖ ^ 2 + 2 * ‖b‖ ^ 2

theorem EulerMeanHarmonic.localL2Energy_add_le (s : Set EulerSmoothLimit.Space) (u v : ↥EulerMeanSolenoidal.L2) : localL2Energy s (u + v) ≤ 2 * localL2Energy s u + 2 * localL2Energy s v

theorem EulerMeanHarmonic.localL2Energy_le_of_decomposition (s : Set EulerSmoothLimit.Space) (z w : ↥EulerMeanSolenoidal.L2) : localL2Energy s z ≤ 2 * localL2Energy s (z - w) + 2 * ‖w‖ ^ 2

theorem EulerMeanHarmonic.localL2Energy_ball_le_of_ae_bound (u : ↥EulerMeanSolenoidal.L2) (C r : ℝ) (hr : 0 ≤ r) (hbound : ∀ᵐ (x : EulerSmoothLimit.Space), x ∈ Metric.ball 0 r → ‖↑↑u x‖ ^ 2 ≤ C) : localL2Energy (Metric.ball 0 r) u ≤ Real.pi * 4 / 3 * r ^ 3 * C