Bookkeeping for the chain of interior estimates

Nested boxes, monotonicity of integrals of nonnegative densities in the domain, and integral bounds from pointwise bounds, used to chain the interior estimates of thm:vorticity-regularity.

theorem ESS.vorticityBox_subset (x₀ : CKN.Foundation.Parabolic.Vec3) {r R a b : ℝ} (t₀ : ℝ) (hrR : r ≤ R) (hab : a ≤ b) : CKN.Foundation.Parabolic.vec3Ball x₀ r ×ˢ Set.Ioo b t₀ ⊆ CKN.Foundation.Parabolic.vec3Ball x₀ R ×ˢ Set.Ioo a t₀

Nested boxes with a common top time.

theorem ESS.vorticity_setIntegral_le_of_subset {S T : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hST : S ⊆ T) {g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : MeasureTheory.IntegrableOn g T MeasureTheory.volume) (h0 : ∀ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), 0 ≤ g z) {K : ℝ} (hK : ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in T, g z ≤ K) : ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in S, g z ≤ K

The integral of a nonnegative density over a subset is bounded by any bound of the integral over the larger set.

theorem ESS.vorticity_integral_le_combo {μ : MeasureTheory.Measure (CKN.Foundation.Parabolic.Vec3 × ℝ)} {f g₁ g₂ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {c₁ c₂ K₁ K₂ : ℝ} (hc₁ : 0 ≤ c₁) (hc₂ : 0 ≤ c₂) (hf0 : ∀ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), 0 ≤ f z) (hg₁ : MeasureTheory.Integrable g₁ μ) (hg₂ : MeasureTheory.Integrable g₂ μ) (hle : ∀ᵐ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) ∂μ, f z ≤ c₁ * g₁ z + c₂ * g₂ z) (h₁ : ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), g₁ z ∂μ ≤ K₁) (h₂ : ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), g₂ z ∂μ ≤ K₂) : ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), f z ∂μ ≤ c₁ * K₁ + c₂ * K₂

An integral bound from a pointwise bound by a combination of two integrable densities.

theorem ESS.vorticity_sq_le_sum_two (f : Fin 3 → Fin 3 → ℝ) (a b : Fin 3) : f a b ^ 2 ≤ ∑ i : Fin 3, ∑ j : Fin 3, f i j ^ 2

One square of a matrix is bounded by the sum of all its squares.

theorem ESS.vorticity_sq_le_sum_three (f : Fin 3 → Fin 3 → Fin 3 → ℝ) (a b c : Fin 3) : f a b c ^ 2 ≤ ∑ i : Fin 3, ∑ j : Fin 3, ∑ k : Fin 3, f i j k ^ 2

One square of a three-index array is bounded by the sum of all its squares.