Integration of periodic fields on the unit cube

The integral is product Lebesgue measure in the usual three coordinates, pulled back along the standard continuous linear equivalence to Euclidean space. Integration by parts is derived from Mathlib's proved box divergence theorem.

@[reducible, inline]

abbrev NavierStokes.PeriodicIntegration.Coords : Type

Coords: an abbreviation for Fin 3 → ℝ.

Equations

• NavierStokes.PeriodicIntegration.Coords = (Fin 3 → ℝ)

noncomputable def NavierStokes.PeriodicIntegration.toSpace : Coords ≃L[ℝ] ProblemStatement.Space

To space, given by (EuclideanSpace.equiv (Fin 3) ℝ).symm.

Equations

• NavierStokes.PeriodicIntegration.toSpace = (EuclideanSpace.equiv (Fin 3) ℝ).symm

def NavierStokes.PeriodicIntegration.cube : Set Coords

Cube, given by Icc 0 1.

Equations

• NavierStokes.PeriodicIntegration.cube = Set.Icc 0 1

noncomputable def NavierStokes.PeriodicIntegration.cubeMeasure : MeasureTheory.Measure Coords

Cube measure, constructed using volume.restrict.

Equations

• NavierStokes.PeriodicIntegration.cubeMeasure = MeasureTheory.volume.restrict NavierStokes.PeriodicIntegration.cube

instance NavierStokes.PeriodicIntegration.instIsFiniteMeasureCoordsCubeMeasure : MeasureTheory.IsFiniteMeasure cubeMeasure

noncomputable def NavierStokes.PeriodicIntegration.cubeIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ProblemStatement.Space → E) : E

Cube integral, given by ∫ y, f (toSpace y) ∂cubeMeasure.

Equations

• NavierStokes.PeriodicIntegration.cubeIntegral f = ∫ (y : NavierStokes.PeriodicIntegration.Coords), f (NavierStokes.PeriodicIntegration.toSpace y) ∂NavierStokes.PeriodicIntegration.cubeMeasure

def NavierStokes.PeriodicIntegration.UnitPeriods {E : Type u_1} (f : ProblemStatement.Space → E) : Prop

Unit periods, given by ∀ x i, f (x + coordinateVector i) = f x.

Equations

• NavierStokes.PeriodicIntegration.UnitPeriods f = ∀ (x : NavierStokes.ProblemStatement.Space) (i : Fin 3), f (x + NavierStokes.ProblemStatement.coordinateVector i) = f x

noncomputable def NavierStokes.PeriodicIntegration.spatialPartial {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (i : Fin 3) (f : ProblemStatement.Space → E) (x : ProblemStatement.Space) : E

Spatial partial, given by fderiv ℝ f x (coordinateVector i).

Equations

• NavierStokes.PeriodicIntegration.spatialPartial i f x = (fderiv ℝ f x) (NavierStokes.ProblemStatement.coordinateVector i)

@[simp]

theorem NavierStokes.PeriodicIntegration.toSpace_apply (y : Coords) (i : Fin 3) : (toSpace y).ofLp i = y i

@[simp]

theorem NavierStokes.PeriodicIntegration.toSpace_single (i : Fin 3) : toSpace (Pi.single i 1) = ProblemStatement.coordinateVector i

theorem NavierStokes.PeriodicIntegration.continuous_partial {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ProblemStatement.Space → E} (hf : ContDiff ℝ 1 f) (i : Fin 3) : Continuous (spatialPartial i f)

theorem NavierStokes.PeriodicIntegration.integrable_cube {E : Type u_1} [NormedAddCommGroup E] {f : ProblemStatement.Space → E} (hf : Continuous f) : MeasureTheory.Integrable (fun (y : Coords) => f (toSpace y)) cubeMeasure

@[simp]

theorem NavierStokes.PeriodicIntegration.cubeIntegral_zero : (cubeIntegral fun (x : ProblemStatement.Space) => 0) = 0

theorem NavierStokes.PeriodicIntegration.cubeIntegral_add {f g : ProblemStatement.Space → ℝ} (hf : Continuous f) (hg : Continuous g) : (cubeIntegral fun (x : ProblemStatement.Space) => f x + g x) = cubeIntegral f + cubeIntegral g

theorem NavierStokes.PeriodicIntegration.cubeIntegral_sub {f g : ProblemStatement.Space → ℝ} (hf : Continuous f) (hg : Continuous g) : (cubeIntegral fun (x : ProblemStatement.Space) => f x - g x) = cubeIntegral f - cubeIntegral g

theorem NavierStokes.PeriodicIntegration.cubeIntegral_neg (f : ProblemStatement.Space → ℝ) : (cubeIntegral fun (x : ProblemStatement.Space) => -f x) = -cubeIntegral f

theorem NavierStokes.PeriodicIntegration.cubeIntegral_const_mul (c : ℝ) (f : ProblemStatement.Space → ℝ) : (cubeIntegral fun (x : ProblemStatement.Space) => c * f x) = c * cubeIntegral f

theorem NavierStokes.PeriodicIntegration.cubeIntegral_sum {ι : Type u_1} (s : Finset ι) (f : ι → ProblemStatement.Space → ℝ) (hf : ∀ i ∈ s, Continuous (f i)) : (cubeIntegral fun (x : ProblemStatement.Space) => ∑ i ∈ s, f i x) = ∑ i ∈ s, cubeIntegral (f i)

theorem NavierStokes.PeriodicIntegration.cubeIntegral_nonneg {f : ProblemStatement.Space → ℝ} (hf : ∀ (x : ProblemStatement.Space), 0 ≤ f x) : 0 ≤ cubeIntegral f

theorem NavierStokes.PeriodicIntegration.cubeIntegral_mono {f g : ProblemStatement.Space → ℝ} (hf : Continuous f) (hg : Continuous g) (hfg : ∀ (x : ProblemStatement.Space), f x ≤ g x) : cubeIntegral f ≤ cubeIntegral g

theorem NavierStokes.PeriodicIntegration.cubeIntegral_nonneg_on_cube {f : ProblemStatement.Space → ℝ} (hf : ∀ y ∈ cube, 0 ≤ f (toSpace y)) : 0 ≤ cubeIntegral f

theorem NavierStokes.PeriodicIntegration.cubeIntegral_mono_on_cube {f g : ProblemStatement.Space → ℝ} (hf : Continuous f) (hg : Continuous g) (hfg : ∀ y ∈ cube, f (toSpace y) ≤ g (toSpace y)) : cubeIntegral f ≤ cubeIntegral g

theorem NavierStokes.PeriodicIntegration.cubeIntegral_partial_eq_zero {f : ProblemStatement.Space → ℝ} (hf : ContDiff ℝ 1 f) (hp : UnitPeriods f) (i : Fin 3) : cubeIntegral (spatialPartial i f) = 0

A genuine coordinate derivative integrates to zero for a C¹ unit-periodic field.

theorem NavierStokes.PeriodicIntegration.partial_mul {f g : ProblemStatement.Space → ℝ} (hf : ContDiff ℝ 1 f) (hg : ContDiff ℝ 1 g) (i : Fin 3) (x : ProblemStatement.Space) : spatialPartial i (fun (y : ProblemStatement.Space) => f y * g y) x = f x * spatialPartial i g x + g x * spatialPartial i f x

theorem NavierStokes.PeriodicIntegration.cubeIntegral_mul_partial {f g : ProblemStatement.Space → ℝ} (hf : ContDiff ℝ 1 f) (hg : ContDiff ℝ 1 g) (hpf : UnitPeriods f) (hpg : UnitPeriods g) (i : Fin 3) : (cubeIntegral fun (x : ProblemStatement.Space) => f x * spatialPartial i g x) = -cubeIntegral fun (x : ProblemStatement.Space) => g x * spatialPartial i f x

Integration by parts for actual coordinate partial derivatives on the unit torus.

theorem NavierStokes.PeriodicIntegration.eq_zero_on_cube_of_nonneg_of_integral_eq_zero {f : ProblemStatement.Space → ℝ} (hf : Continuous f) (hn : ∀ (x : ProblemStatement.Space), 0 ≤ f x) (hz : cubeIntegral f = 0) (y : Coords) : y ∈ cube → f (toSpace y) = 0

Zero integral of a continuous nonnegative field implies zero at every point of the closed cube, including its faces.

theorem NavierStokes.PeriodicIntegration.eq_zero_on_cube_of_integral_norm_sq_eq_zero {E : Type u_1} [NormedAddCommGroup E] {u : ProblemStatement.Space → E} (hu : Continuous u) (hz : (cubeIntegral fun (x : ProblemStatement.Space) => ‖u x‖ ^ 2) = 0) (y : Coords) : y ∈ cube → u (toSpace y) = 0

theorem NavierStokes.PeriodicIntegration.cubeIntegral_continuousOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {I : Set ℝ} {F : ℝ × ProblemStatement.Space → E} (hI : IsCompact I) (hF : ContinuousOn F (I ×ˢ Set.univ)) : ContinuousOn (fun (t : ℝ) => cubeIntegral fun (x : ProblemStatement.Space) => F (t, x)) I

Joint continuity on a compact time interval gives continuity of the actual cube integral, including at the endpoints.

theorem NavierStokes.PeriodicIntegration.cubeIntegral_continuousOn_Icc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : ℝ × ProblemStatement.Space → E} {a b : ℝ} (hF : ContinuousOn F (Set.Icc a b ×ˢ Set.univ)) : ContinuousOn (fun (t : ℝ) => cubeIntegral fun (x : ProblemStatement.Space) => F (t, x)) (Set.Icc a b)

theorem NavierStokes.PeriodicIntegration.hasDerivAt_cubeIntegral_of_hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {I : Set ℝ} {F G : ℝ × ProblemStatement.Space → E} (hI : IsOpen I) (hF : ContinuousOn F (I ×ˢ Set.univ)) (hG : ContinuousOn G (I ×ˢ Set.univ)) (hd : ∀ t ∈ I, ∀ (x : ProblemStatement.Space), HasDerivAt (fun (s : ℝ) => F (s, x)) (G (t, x)) t) {t : ℝ} (ht : t ∈ I) : HasDerivAt (fun (s : ℝ) => cubeIntegral fun (x : ProblemStatement.Space) => F (s, x)) (cubeIntegral fun (x : ProblemStatement.Space) => G (t, x)) t

Compactness of the cube supplies the local integrable derivative majorant. The derivative premise is the ordinary pointwise derivative of the integrand.

theorem NavierStokes.PeriodicIntegration.hasDerivAt_cubeIntegral_of_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {I : Set ℝ} {F : ℝ × ProblemStatement.Space → E} (hI : IsOpen I) (hF : ContDiffOn ℝ 1 F (I ×ˢ Set.univ)) {t : ℝ} (ht : t ∈ I) : HasDerivAt (fun (s : ℝ) => cubeIntegral fun (x : ProblemStatement.Space) => F (s, x)) (cubeIntegral fun (x : ProblemStatement.Space) => deriv (fun (s : ℝ) => F (s, x)) t) t

Differentiation under the cube integral for a jointly C¹ field on an open time domain. The integrated quantity is its actual time-slice derivative.