Unit-cube integration with product Lebesgue measure and coordinate-by-coordinate Fubini formulas.

noncomputable def KamProject.Arnold1963.unitIntervalMeasure : MeasureTheory.Measure ℝ

Lebesgue probability measure restricted to the closed unit interval.

Equations

• KamProject.Arnold1963.unitIntervalMeasure = MeasureTheory.volume.restrict (Set.Icc 0 1)

instance KamProject.Arnold1963.instIsProbabilityMeasureRealUnitIntervalMeasure : MeasureTheory.IsProbabilityMeasure unitIntervalMeasure

noncomputable def KamProject.Arnold1963.unitCubeMeasure (n : ℕ) : MeasureTheory.Measure (RealSpace n)

Product probability measure on the unit cube, used for normalized Fourier integration.

Equations

• KamProject.Arnold1963.unitCubeMeasure n = MeasureTheory.Measure.pi fun (x : Fin n) => KamProject.Arnold1963.unitIntervalMeasure

instance KamProject.Arnold1963.instIsProbabilityMeasureRealSpaceUnitCubeMeasure (n : ℕ) : MeasureTheory.IsProbabilityMeasure (unitCubeMeasure n)

def KamProject.Arnold1963.unitCube (n : ℕ) : Set (RealSpace n)

The closed unit cube in real coordinate space.

Equations

• KamProject.Arnold1963.unitCube n = Set.univ.pi fun (x : Fin n) => Set.Icc 0 1

noncomputable def KamProject.Arnold1963.unitCubeIntegral {n : ℕ} (f : RealSpace n → ℂ) : ℂ

Integration over the unit cube with its product probability measure.

Equations

• KamProject.Arnold1963.unitCubeIntegral f = ∫ (x : KamProject.Arnold1963.RealSpace n), f x ∂KamProject.Arnold1963.unitCubeMeasure n

theorem KamProject.Arnold1963.unitCubeMeasure_eq_restrict (n : ℕ) : unitCubeMeasure n = MeasureTheory.volume.restrict (unitCube n)

theorem KamProject.Arnold1963.ae_mem_unitCube (n : ℕ) : ∀ᵐ (x : RealSpace n) ∂unitCubeMeasure n, x ∈ unitCube n

theorem KamProject.Arnold1963.integrable_unitCube {n : ℕ} {f : RealSpace n → ℂ} (hf : ContinuousOn f (unitCube n)) : MeasureTheory.Integrable f (unitCubeMeasure n)

theorem KamProject.Arnold1963.unitCubeIntegral_congr {n : ℕ} {f g : RealSpace n → ℂ} (h : ∀ x ∈ unitCube n, f x = g x) : unitCubeIntegral f = unitCubeIntegral g

theorem KamProject.Arnold1963.norm_unitCubeIntegral_le {n : ℕ} {f : RealSpace n → ℂ} {M : ℝ} (h : ∀ x ∈ unitCube n, ‖f x‖ ≤ M) : ‖unitCubeIntegral f‖ ≤ M

theorem KamProject.Arnold1963.integrable_cons_unitCube {n : ℕ} {f : RealSpace (n + 1) → ℂ} (hf : MeasureTheory.Integrable f (unitCubeMeasure (n + 1))) : MeasureTheory.Integrable (fun (xy : ℝ × RealSpace n) => f (Fin.cons xy.1 xy.2)) (unitIntervalMeasure.prod (unitCubeMeasure n))

theorem KamProject.Arnold1963.unitCubeIntegral_cons {n : ℕ} {f : RealSpace (n + 1) → ℂ} (hf : MeasureTheory.Integrable f (unitCubeMeasure (n + 1))) : unitCubeIntegral f = ∫ (x : ℝ), unitCubeIntegral fun (y : RealSpace n) => f (Fin.cons x y) ∂unitIntervalMeasure

theorem KamProject.Arnold1963.unitCubeIntegral_cons_symm {n : ℕ} {f : RealSpace (n + 1) → ℂ} (hf : MeasureTheory.Integrable f (unitCubeMeasure (n + 1))) : unitCubeIntegral f = ∫ (y : RealSpace n), ∫ (x : ℝ), f (Fin.cons x y) ∂unitIntervalMeasure ∂unitCubeMeasure n

theorem KamProject.Arnold1963.integral_unitInterval_eq_interval (f : ℝ → ℂ) : ∫ (x : ℝ), f x ∂unitIntervalMeasure = ∫ (x : ℝ) in 0..1, f x

theorem KamProject.Arnold1963.unitCubeMeasure_eq_restrict_Ioc (n : ℕ) : unitCubeMeasure n = MeasureTheory.volume.restrict {x : RealSpace n | ∀ (j : Fin n), x j ∈ Set.Ioc 0 1}