Dimensional invarance of the integral #
In this module we prove that the dimensional properties of the integral.
noncomputable instance
instMulUnitDependentMeasureOfModuleCarriesDimensionOfMeasurableConstSMulReal
(M : Type)
[NormedAddCommGroup M]
[NormedSpace ℝ M]
[ModuleCarriesDimension M]
[MeasurableSpace M]
[self : MeasurableConstSMul ℝ M]
:
Equations
- One or more equations did not get rendered due to their size.
theorem
scaleUnit_measure
{M : Type}
[NormedAddCommGroup M]
[NormedSpace ℝ M]
[ModuleCarriesDimension M]
[MeasurableSpace M]
[MeasurableConstSMul ℝ M]
(u1 u2 : UnitChoices)
(μ : MeasureTheory.Measure M)
:
UnitDependent.scaleUnit u1 u2 μ = MeasureTheory.Measure.map (fun (m : M) => UnitDependent.scaleUnit u1 u2 m) μ
theorem
integral_isDimensionallyCorrect
{M : Type}
[NormedAddCommGroup M]
[NormedSpace ℝ M]
[ModuleCarriesDimension M]
[MeasurableSpace M]
[MeasurableConstSMul ℝ M]
{G : Type}
[NormedAddCommGroup G]
[NormedSpace ℝ G]
[ModuleCarriesDimension G]
(d : Dimension)
:
IsDimensionallyCorrect
fun (μ : ↑(DimSet (MeasureTheory.Measure M) d)) (f : ↑(DimSet (M → G) (CarriesDimension.d G * d⁻¹))) =>
∫ (x : M), ↑f x ∂↑μ
The statement that for a measure μ of dimension d, and a function
f : M → G of dimension (CarriesDimension.d G * d⁻¹) (where CarriesDimension.d G
is the dimension associated with terms of type G), then
∫ x, f x ∂μ
has the correct dimension, namely CarriesDimension.d G.
In other words, the function:
fun (μ : DimSet (MeasureTheory.Measure M) d)
(f : DimSet (M → G) (CarriesDimension.d G * d⁻¹)) ↦ ∫ x, f.1 x ∂μ.1
is dimensionally correct.