Jointly measurable representatives of weakly continuous slices

Ball averages turn a weakly continuous family of spatial L³ classes into a jointly measurable pointwise field without changing any time slice almost everywhere.

theorem instFactLeENNRealOfNatOfRealHDivReal_leanPool_2 : Fact (1 ≤ ENNReal.ofReal (3 / 2))

theorem instFactLeENNRealOfNat_leanPool_3 : Fact (1 ≤ 2)

def ESS.blowupRepresentativeDomain : Set CKN.Foundation.Parabolic.Vec3

The spatial ball on which the blow-up representative is defined.

Equations

• ESS.blowupRepresentativeDomain = CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4)

noncomputable def ESS.blowupRepresentativeRadius (n : ℕ) : ℝ

The positive radii tending to zero used to form local averages.

Equations

• ESS.blowupRepresentativeRadius n = (↑n + 1)⁻¹

def ESS.blowupRepresentativeBall (x : CKN.Foundation.Parabolic.Vec3) (n : ℕ) : Set CKN.Foundation.Parabolic.Vec3

The closed ball centered at x with the nth averaging radius.

Equations

• ESS.blowupRepresentativeBall x n = Metric.closedBall x (ESS.blowupRepresentativeRadius n)

def ESS.blowupRepresentativeTestSet (x : CKN.Foundation.Parabolic.Vec3) (n : ℕ) : Set CKN.Foundation.Parabolic.Vec3

The part of the averaging ball contained in the representative domain.

Equations

• ESS.blowupRepresentativeTestSet x n = ESS.blowupRepresentativeDomain ∩ ESS.blowupRepresentativeBall x n

@[reducible, inline]

noncomputable abbrev ESS.blowupRepresentativeMeasure : MeasureTheory.Measure CKN.Foundation.Parabolic.Vec3

Volume restricted to the spatial domain of the representative.

Equations

• ESS.blowupRepresentativeMeasure = MeasureTheory.volume.restrict ESS.blowupRepresentativeDomain

theorem ESS.blowupRepresentative_testSet_finite (x : CKN.Foundation.Parabolic.Vec3) (n : ℕ) : blowupRepresentativeMeasure (blowupRepresentativeTestSet x n) ≠ ⊤

noncomputable def ESS.blowupRepresentativeIndicator (n : ℕ) (x : CKN.Foundation.Parabolic.Vec3) (i : Fin 3) : ↥(MeasureTheory.Lp CKN.Foundation.Parabolic.L2Vec3 (ENNReal.ofReal (3 / 2)) blowupRepresentativeMeasure)

The constant coordinate test on the local test set in the dual L^{3/2} space.

Equations

• ESS.blowupRepresentativeIndicator n x i = MeasureTheory.indicatorConstLp (ENNReal.ofReal (3 / 2)) ⋯ ⋯ (CKN.weakContL3VecToLp (Pi.single i 1))

noncomputable def ESS.blowupRepresentativeCoordinateAverage (v : ↑(Set.Icc (-(3 / 4) ^ 2) 0) → ↥(MeasureTheory.Lp CKN.Foundation.Parabolic.L2Vec3 3 blowupRepresentativeMeasure)) (n : ℕ) (x : CKN.Foundation.Parabolic.Vec3) (t : ↑(Set.Icc (-(3 / 4) ^ 2) 0)) (i : Fin 3) : ℝ

The normalized integral of one velocity coordinate over the local test set.

Equations

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

noncomputable def ESS.blowupRepresentativeApprox (v : ↑(Set.Icc (-(3 / 4) ^ 2) 0) → ↥(MeasureTheory.Lp CKN.Foundation.Parabolic.L2Vec3 3 blowupRepresentativeMeasure)) (n : ℕ) (x : CKN.Foundation.Parabolic.Vec3) (t : ↑(Set.Icc (-(3 / 4) ^ 2) 0)) : CKN.Foundation.Parabolic.Vec3

The vector of coordinate averages at radius indexed by n.

Equations

• ESS.blowupRepresentativeApprox v n x t i = ESS.blowupRepresentativeCoordinateAverage v n x t i

noncomputable def ESS.blowupRepresentativeRaw (v : ↑(Set.Icc (-(3 / 4) ^ 2) 0) → ↥(MeasureTheory.Lp CKN.Foundation.Parabolic.L2Vec3 3 blowupRepresentativeMeasure)) (t : ↑(Set.Icc (-(3 / 4) ^ 2) 0)) (x : CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.Vec3

The weakly continuous slice, set to zero outside its domain.

Equations

• ESS.blowupRepresentativeRaw v t x = ESS.blowupRepresentativeDomain.indicator (fun (y : CKN.Foundation.Parabolic.Vec3) => CKN.weakContL3OfLp (↑↑(v t) y)) x

noncomputable def ESS.blowupRepresentativePairing (f : ↥(MeasureTheory.Lp CKN.Foundation.Parabolic.L2Vec3 3 blowupRepresentativeMeasure)) : ↥(MeasureTheory.Lp CKN.Foundation.Parabolic.L2Vec3 (ENNReal.ofReal (3 / 2)) blowupRepresentativeMeasure) → ℝ

The integral pairing of an L³ field with an L^{3/2} test on the restricted domain.

Equations

• ESS.blowupRepresentativePairing f g = ∫ (y : CKN.Foundation.Parabolic.Vec3), inner ℝ (↑↑f y) (↑↑g y) ∂ESS.blowupRepresentativeMeasure

theorem ESS.weakContL3_jointlyMeasurableRepresentative (v : ↑(Set.Icc (-(3 / 4) ^ 2) 0) → ↥(MeasureTheory.Lp CKN.Foundation.Parabolic.L2Vec3 3 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4))))) (hweak : ∀ (w : ↥(MeasureTheory.Lp CKN.Foundation.Parabolic.L2Vec3 (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4))))), Continuous fun (t : ↑(Set.Icc (-(3 / 4) ^ 2) 0)) => ∫ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4), inner ℝ (↑↑(v t) x) (↑↑w x)) : ∃ (W : CKN.Foundation.Parabolic.Vec3 × ↑(Set.Icc (-(3 / 4) ^ 2) 0) → CKN.Foundation.Parabolic.Vec3), Measurable W ∧ ∀ (t : ↑(Set.Icc (-(3 / 4) ^ 2) 0)), (fun (x : CKN.Foundation.Parabolic.Vec3) => W (x, t)) =ᵐ[MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4))] fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.weakContL3OfLp (↑↑(v t) x)

Weakly continuous local L³ slices have a jointly measurable pointwise representative whose every time slice agrees almost everywhere with the given class. The representative is obtained from spatial ball averages and Lebesgue differentiation.