Commutator L2 Sq Congr

Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.

theorem CIV.diPernaLionsCommutator_congr_ae_slice {m : ℕ} {ε : ℝ} {b : CKN.Vec m → CKN.Vec m} {divb g g' : CKN.Vec m → ℝ} (h : g =ᵐ[MeasureTheory.volume] g') (x : CKN.Vec m) : diPernaLionsCommutator m ε b divb g x = diPernaLionsCommutator m ε b divb g' x

The DiPerna–Lions commutator is unchanged when the transported function g is replaced by an a.e.-equal representative on a single spatial slice.

theorem CIV.commutatorL2Sq_congr_ae_slice {m : ℕ} {ε Rb s : ℝ} {B : CKN.Vec m × ℝ → CKN.Vec m} {divB q q' : CKN.Vec m × ℝ → ℝ} (h : (fun (y : CKN.Vec m) => q (y, s)) =ᵐ[MeasureTheory.volume] fun (y : CKN.Vec m) => q' (y, s)) : commutatorL2Sq m ε Rb B divB q s = commutatorL2Sq m ε Rb B divB q' s

The squared L² mass on a ball of the DiPerna–Lions commutator is unchanged when the transported function q is replaced by an a.e.-equal representative on a single time slice.

theorem CIV.sqrt_commutatorL2Sq_congr_ae_slice {m : ℕ} {ε Rb s : ℝ} {B : CKN.Vec m × ℝ → CKN.Vec m} {divB q q' : CKN.Vec m × ℝ → ℝ} (h : (fun (y : CKN.Vec m) => q (y, s)) =ᵐ[MeasureTheory.volume] fun (y : CKN.Vec m) => q' (y, s)) : √(commutatorL2Sq m ε Rb B divB q s) = √(commutatorL2Sq m ε Rb B divB q' s)

The square root of the squared L² mass of the commutator is unchanged when the transported function q is replaced by an a.e.-equal representative on a single time slice.

theorem CIV.commutatorL2Sq_eqOn_of_forall_ae_slice {m : ℕ} {ε Rb : ℝ} {S : Set ℝ} {B : CKN.Vec m × ℝ → CKN.Vec m} {divB q q' : CKN.Vec m × ℝ → ℝ} (h : ∀ s ∈ S, (fun (y : CKN.Vec m) => q (y, s)) =ᵐ[MeasureTheory.volume] fun (y : CKN.Vec m) => q' (y, s)) : Set.EqOn (fun (s : ℝ) => commutatorL2Sq m ε Rb B divB q s) (fun (s : ℝ) => commutatorL2Sq m ε Rb B divB q' s) S

The squared L² mass of the commutator is equal on a set S whenever q and q' agree a.e. on every slice s ∈ S.

theorem CIV.continuousOn_sqrt_commutatorL2Sq_congr {m : ℕ} {ε Rb : ℝ} {S : Set ℝ} {B : CKN.Vec m × ℝ → CKN.Vec m} {divB q q' : CKN.Vec m × ℝ → ℝ} (h : ∀ s ∈ S, (fun (y : CKN.Vec m) => q (y, s)) =ᵐ[MeasureTheory.volume] fun (y : CKN.Vec m) => q' (y, s)) (hcont : ContinuousOn (fun (s : ℝ) => √(commutatorL2Sq m ε Rb B divB q' s)) S) : ContinuousOn (fun (s : ℝ) => √(commutatorL2Sq m ε Rb B divB q s)) S

If the square root of the commutator mass for q' is continuous on S, then so is it for any q that agrees with q' a.e. on each slice in S.