Physlib.Units.Integral

Physlib
Units
Integral

Imports

/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.Units.UnitDependent
public import Mathlib.MeasureTheory.Integral.Bochner.Basic

Dimensional invariance of the integral

In this module we prove that the dimensional properties of the integral.

@[expose] public section

lemma scaleUnit_measure (u1 u2 : LTMCTUnitChoices) (μ : MeasureTheory.Measure M) :
    scaleUnit u1 u2 μ = μ.map (fun m => scaleUnit u1 u2 m) := byM:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:HasDim Minst✝¹:MeasurableSpace Minst✝:MeasurableConstSMul ℝ Mu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesμ:Measure M⊢ scaleUnit u1 u2 μ = Measure.map (fun m => scaleUnit u1 u2 m) μ rflAll goals completed! 🐙

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.


lemma integral_isDimensionallyCorrect (d : Dimension LTMCTDimensionBase) :
    IsDimensionallyCorrect (fun (μ : DimSet (MeasureTheory.Measure M) d)
      (f : DimSet (M → G) (dim G * d⁻¹)) ↦ ∫ x, f.1 x ∂μ.1) := byM:Typeinst✝⁷:NormedAddCommGroup Minst✝⁶:NormedSpace ℝ Minst✝⁵:HasDim Minst✝⁴:MeasurableSpace Minst✝³:MeasurableConstSMul ℝ MG:Typeinst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace ℝ Ginst✝:HasDim Gd:Dimension LTMCTDimensionBase⊢ IsDimensionallyCorrect fun μ f => ∫ (x : M), ↑f x ∂↑μ
  intro u1 u2M:Typeinst✝⁷:NormedAddCommGroup Minst✝⁶:NormedSpace ℝ Minst✝⁵:HasDim Minst✝⁴:MeasurableSpace Minst✝³:MeasurableConstSMul ℝ MG:Typeinst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace ℝ Ginst✝:HasDim Gd:Dimension LTMCTDimensionBaseu1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ (scaleUnit u1 u2 fun μ f => ∫ (x : M), ↑f x ∂↑μ) = fun μ f => ∫ (x : M), ↑f x ∂↑μ
  funext ⟨μ, hμ⟩ ⟨f, hf⟩M:Typeinst✝⁷:NormedAddCommGroup Minst✝⁶:NormedSpace ℝ Minst✝⁵:HasDim Minst✝⁴:MeasurableSpace Minst✝³:MeasurableConstSMul ℝ MG:Typeinst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace ℝ Ginst✝:HasDim Gd:Dimension LTMCTDimensionBaseu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesμ:Measure Mhμ:μ ∈ DimSet (Measure M) df:M → Ghf:f ∈ DimSet (M → G) (dim G * d⁻¹)⊢ scaleUnit u1 u2 (fun μ f => ∫ (x : M), ↑f x ∂↑μ) ⟨μ, hμ⟩ ⟨f, hf⟩ = ∫ (x : M), ↑⟨f, hf⟩ x ∂↑⟨μ, hμ⟩
  /- We have to prove that
    `scaleUnit u1 (fun μ f ↦ ∫ x, f x ∂μ) u2 ⟨μ, hμ⟩ ⟨f, hf⟩ = ∫ x, f x ∂μ` -/
  calc _
    /- By definition the LHS is equal to
    `scaleUnit u1 u2 (∫ x, (scaleUnit u2 u1 f) x ∂(scaleUnit u2 u1 μ)) `
    The statement says, suppose `f` and `μ` are in units `u2`, we change them to units `u1`,
    then do the integral, and then we take the result back to `u2`.
    If the integral is dimensionally correct, this should be the same as just doing the
    original integral in `u2` units i.e. `∫ x, f x ∂μ`. -/
    _ = scaleUnit u1 u2 (∫ x, (scaleUnit u2 u1 f) x ∂(scaleUnit u2 u1 μ)) := byM:Typeinst✝⁷:NormedAddCommGroup Minst✝⁶:NormedSpace ℝ Minst✝⁵:HasDim Minst✝⁴:MeasurableSpace Minst✝³:MeasurableConstSMul ℝ MG:Typeinst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace ℝ Ginst✝:HasDim Gd:Dimension LTMCTDimensionBaseu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesμ:Measure Mhμ:μ ∈ DimSet (Measure M) df:M → Ghf:f ∈ DimSet (M → G) (dim G * d⁻¹)⊢ scaleUnit u1 u2 (fun μ f => ∫ (x : M), ↑f x ∂↑μ) ⟨μ, hμ⟩ ⟨f, hf⟩ =
  scaleUnit u1 u2 (∫ (x : M), scaleUnit u2 u1 f x ∂scaleUnit u2 u1 μ)
      simpAll goals completed! 🐙
    /- Since we have assumed `μ` has dimension `d`, `(scaleUnit u2 μ u1)`
      is equal to `(u2.dimScale u1 d) • μ` -/
    _ = scaleUnit u1 u2 (u2.dimScale u1 d • ∫ (x : M), scaleUnit u2 u1 f x ∂ μ) := byM:Typeinst✝⁷:NormedAddCommGroup Minst✝⁶:NormedSpace ℝ Minst✝⁵:HasDim Minst✝⁴:MeasurableSpace Minst✝³:MeasurableConstSMul ℝ MG:Typeinst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace ℝ Ginst✝:HasDim Gd:Dimension LTMCTDimensionBaseu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesμ:Measure Mhμ:μ ∈ DimSet (Measure M) df:M → Ghf:f ∈ DimSet (M → G) (dim G * d⁻¹)⊢ scaleUnit u1 u2 (∫ (x : M), scaleUnit u2 u1 f x ∂scaleUnit u2 u1 μ) =
  scaleUnit u1 u2 ((u2.dimScale u1) d • ∫ (x : M), scaleUnit u2 u1 f x ∂μ)
      rw [hμ,M:Typeinst✝⁷:NormedAddCommGroup Minst✝⁶:NormedSpace ℝ Minst✝⁵:HasDim Minst✝⁴:MeasurableSpace Minst✝³:MeasurableConstSMul ℝ MG:Typeinst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace ℝ Ginst✝:HasDim Gd:Dimension LTMCTDimensionBaseu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesμ:Measure Mhμ:μ ∈ DimSet (Measure M) df:M → Ghf:f ∈ DimSet (M → G) (dim G * d⁻¹)⊢ scaleUnit u1 u2 (∫ (x : M), scaleUnit u2 u1 f x ∂(u2.dimScale u1) d • μ) =
  scaleUnit u1 u2 ((u2.dimScale u1) d • ∫ (x : M), scaleUnit u2 u1 f x ∂μ)All goals completed! 🐙 integral_smul_nnreal_measureM:Typeinst✝⁷:NormedAddCommGroup Minst✝⁶:NormedSpace ℝ Minst✝⁵:HasDim Minst✝⁴:MeasurableSpace Minst✝³:MeasurableConstSMul ℝ MG:Typeinst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace ℝ Ginst✝:HasDim Gd:Dimension LTMCTDimensionBaseu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesμ:Measure Mhμ:μ ∈ DimSet (Measure M) df:M → Ghf:f ∈ DimSet (M → G) (dim G * d⁻¹)⊢ scaleUnit u1 u2 ((u2.dimScale u1) d • ∫ (x : M), scaleUnit u2 u1 f x ∂μ) =
  scaleUnit u1 u2 ((u2.dimScale u1) d • ∫ (x : M), scaleUnit u2 u1 f x ∂μ)All goals completed! 🐙]All goals completed! 🐙
    /- Since we assumed `f` has dimension `CarriesDimension.d G * d⁻¹`, `(scaleUnit u2 f u1)`
      is equal to `u2.dimScale u1 (CarriesDimension.d G * d⁻¹) • f`. -/
    _ = scaleUnit u1 u2 (u2.dimScale u1 d •
      u2.dimScale u1 (dim G * d⁻¹) • ∫ (x : M), f x ∂ μ) := byM:Typeinst✝⁷:NormedAddCommGroup Minst✝⁶:NormedSpace ℝ Minst✝⁵:HasDim Minst✝⁴:MeasurableSpace Minst✝³:MeasurableConstSMul ℝ MG:Typeinst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace ℝ Ginst✝:HasDim Gd:Dimension LTMCTDimensionBaseu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesμ:Measure Mhμ:μ ∈ DimSet (Measure M) df:M → Ghf:f ∈ DimSet (M → G) (dim G * d⁻¹)⊢ scaleUnit u1 u2 ((u2.dimScale u1) d • ∫ (x : M), scaleUnit u2 u1 f x ∂μ) =
  scaleUnit u1 u2 ((u2.dimScale u1) d • (u2.dimScale u1) (dim G * d⁻¹) • ∫ (x : M), f x ∂μ)
      rw [hfM:Typeinst✝⁷:NormedAddCommGroup Minst✝⁶:NormedSpace ℝ Minst✝⁵:HasDim Minst✝⁴:MeasurableSpace Minst✝³:MeasurableConstSMul ℝ MG:Typeinst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace ℝ Ginst✝:HasDim Gd:Dimension LTMCTDimensionBaseu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesμ:Measure Mhμ:μ ∈ DimSet (Measure M) df:M → Ghf:f ∈ DimSet (M → G) (dim G * d⁻¹)⊢ scaleUnit u1 u2 ((u2.dimScale u1) d • ∫ (x : M), ((u2.dimScale u1) (dim G * d⁻¹) • f) x ∂μ) =
  scaleUnit u1 u2 ((u2.dimScale u1) d • (u2.dimScale u1) (dim G * d⁻¹) • ∫ (x : M), f x ∂μ)M:Typeinst✝⁷:NormedAddCommGroup Minst✝⁶:NormedSpace ℝ Minst✝⁵:HasDim Minst✝⁴:MeasurableSpace Minst✝³:MeasurableConstSMul ℝ MG:Typeinst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace ℝ Ginst✝:HasDim Gd:Dimension LTMCTDimensionBaseu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesμ:Measure Mhμ:μ ∈ DimSet (Measure M) df:M → Ghf:f ∈ DimSet (M → G) (dim G * d⁻¹)⊢ scaleUnit u1 u2 ((u2.dimScale u1) d • ∫ (x : M), ((u2.dimScale u1) (dim G * d⁻¹) • f) x ∂μ) =
  scaleUnit u1 u2 ((u2.dimScale u1) d • (u2.dimScale u1) (dim G * d⁻¹) • ∫ (x : M), f x ∂μ)]M:Typeinst✝⁷:NormedAddCommGroup Minst✝⁶:NormedSpace ℝ Minst✝⁵:HasDim Minst✝⁴:MeasurableSpace Minst✝³:MeasurableConstSMul ℝ MG:Typeinst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace ℝ Ginst✝:HasDim Gd:Dimension LTMCTDimensionBaseu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesμ:Measure Mhμ:μ ∈ DimSet (Measure M) df:M → Ghf:f ∈ DimSet (M → G) (dim G * d⁻¹)⊢ scaleUnit u1 u2 ((u2.dimScale u1) d • ∫ (x : M), ((u2.dimScale u1) (dim G * d⁻¹) • f) x ∂μ) =
  scaleUnit u1 u2 ((u2.dimScale u1) d • (u2.dimScale u1) (dim G * d⁻¹) • ∫ (x : M), f x ∂μ)
      congre_a.e_aM:Typeinst✝⁷:NormedAddCommGroup Minst✝⁶:NormedSpace ℝ Minst✝⁵:HasDim Minst✝⁴:MeasurableSpace Minst✝³:MeasurableConstSMul ℝ MG:Typeinst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace ℝ Ginst✝:HasDim Gd:Dimension LTMCTDimensionBaseu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesμ:Measure Mhμ:μ ∈ DimSet (Measure M) df:M → Ghf:f ∈ DimSet (M → G) (dim G * d⁻¹)⊢ ∫ (x : M), ((u2.dimScale u1) (dim G * d⁻¹) • f) x ∂μ = (u2.dimScale u1) (dim G * d⁻¹) • ∫ (x : M), f x ∂μ
      erw [MeasureTheory.integral_smule_a.e_aM:Typeinst✝⁷:NormedAddCommGroup Minst✝⁶:NormedSpace ℝ Minst✝⁵:HasDim Minst✝⁴:MeasurableSpace Minst✝³:MeasurableConstSMul ℝ MG:Typeinst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace ℝ Ginst✝:HasDim Gd:Dimension LTMCTDimensionBaseu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesμ:Measure Mhμ:μ ∈ DimSet (Measure M) df:M → Ghf:f ∈ DimSet (M → G) (dim G * d⁻¹)⊢ ↑((u2.dimScale u1) (dim G * d⁻¹)) • ∫ (a : M), f a ∂μ = (u2.dimScale u1) (dim G * d⁻¹) • ∫ (x : M), f x ∂μ]e_a.e_aM:Typeinst✝⁷:NormedAddCommGroup Minst✝⁶:NormedSpace ℝ Minst✝⁵:HasDim Minst✝⁴:MeasurableSpace Minst✝³:MeasurableConstSMul ℝ MG:Typeinst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace ℝ Ginst✝:HasDim Gd:Dimension LTMCTDimensionBaseu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesμ:Measure Mhμ:μ ∈ DimSet (Measure M) df:M → Ghf:f ∈ DimSet (M → G) (dim G * d⁻¹)⊢ ↑((u2.dimScale u1) (dim G * d⁻¹)) • ∫ (a : M), f a ∂μ = (u2.dimScale u1) (dim G * d⁻¹) • ∫ (x : M), f x ∂μ
      rflAll goals completed! 🐙
    /- What remains is a simple cancellation of the dimensional scales. -/
    _ = (u1.dimScale u2 (dim G)) • ((u2.dimScale u1 d) •
        u2.dimScale u1 (dim G * d⁻¹) • ∫ (x : M), f x ∂ μ) := byM:Typeinst✝⁷:NormedAddCommGroup Minst✝⁶:NormedSpace ℝ Minst✝⁵:HasDim Minst✝⁴:MeasurableSpace Minst✝³:MeasurableConstSMul ℝ MG:Typeinst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace ℝ Ginst✝:HasDim Gd:Dimension LTMCTDimensionBaseu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesμ:Measure Mhμ:μ ∈ DimSet (Measure M) df:M → Ghf:f ∈ DimSet (M → G) (dim G * d⁻¹)⊢ scaleUnit u1 u2 ((u2.dimScale u1) d • (u2.dimScale u1) (dim G * d⁻¹) • ∫ (x : M), f x ∂μ) =
  (u1.dimScale u2) (dim G) • (u2.dimScale u1) d • (u2.dimScale u1) (dim G * d⁻¹) • ∫ (x : M), f x ∂μ
      rw [← HasDim.scaleUnit_applyM:Typeinst✝⁷:NormedAddCommGroup Minst✝⁶:NormedSpace ℝ Minst✝⁵:HasDim Minst✝⁴:MeasurableSpace Minst✝³:MeasurableConstSMul ℝ MG:Typeinst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace ℝ Ginst✝:HasDim Gd:Dimension LTMCTDimensionBaseu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesμ:Measure Mhμ:μ ∈ DimSet (Measure M) df:M → Ghf:f ∈ DimSet (M → G) (dim G * d⁻¹)⊢ scaleUnit u1 u2 ((u2.dimScale u1) d • (u2.dimScale u1) (dim G * d⁻¹) • ∫ (x : M), f x ∂μ) =
  scaleUnit u1 u2 ((u2.dimScale u1) d • (u2.dimScale u1) (dim G * d⁻¹) • ∫ (x : M), f x ∂μ)All goals completed! 🐙]All goals completed! 🐙
    _ = (u1.dimScale u2 (dim G) * (u2.dimScale u1 d) *
        u2.dimScale u1 (dim G * d⁻¹)) • ∫ (x : M), f x ∂ μ := byM:Typeinst✝⁷:NormedAddCommGroup Minst✝⁶:NormedSpace ℝ Minst✝⁵:HasDim Minst✝⁴:MeasurableSpace Minst✝³:MeasurableConstSMul ℝ MG:Typeinst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace ℝ Ginst✝:HasDim Gd:Dimension LTMCTDimensionBaseu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesμ:Measure Mhμ:μ ∈ DimSet (Measure M) df:M → Ghf:f ∈ DimSet (M → G) (dim G * d⁻¹)⊢ (u1.dimScale u2) (dim G) • (u2.dimScale u1) d • (u2.dimScale u1) (dim G * d⁻¹) • ∫ (x : M), f x ∂μ =
  ((u1.dimScale u2) (dim G) * (u2.dimScale u1) d * (u2.dimScale u1) (dim G * d⁻¹)) • ∫ (x : M), f x ∂μ
      simp [smul_smul]M:Typeinst✝⁷:NormedAddCommGroup Minst✝⁶:NormedSpace ℝ Minst✝⁵:HasDim Minst✝⁴:MeasurableSpace Minst✝³:MeasurableConstSMul ℝ MG:Typeinst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace ℝ Ginst✝:HasDim Gd:Dimension LTMCTDimensionBaseu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesμ:Measure Mhμ:μ ∈ DimSet (Measure M) df:M → Ghf:f ∈ DimSet (M → G) (dim G * d⁻¹)⊢ ((u1.dimScale u2) (dim G) * ((u2.dimScale u1) d * ((u2.dimScale u1) (dim G) * ((u2.dimScale u1) d)⁻¹))) •
    ∫ (x : M), f x ∂μ =
  ((u1.dimScale u2) (dim G) * (u2.dimScale u1) d * ((u2.dimScale u1) (dim G) * ((u2.dimScale u1) d)⁻¹)) •
    ∫ (x : M), f x ∂μ
      ring_nfAll goals completed! 🐙
    _ = ((u1.dimScale u2 (dim G) * u2.dimScale u1 (dim G))
        * (u2.dimScale u1 d * u1.dimScale u2 d)) • ∫ (x : M), f x ∂ μ := byM:Typeinst✝⁷:NormedAddCommGroup Minst✝⁶:NormedSpace ℝ Minst✝⁵:HasDim Minst✝⁴:MeasurableSpace Minst✝³:MeasurableConstSMul ℝ MG:Typeinst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace ℝ Ginst✝:HasDim Gd:Dimension LTMCTDimensionBaseu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesμ:Measure Mhμ:μ ∈ DimSet (Measure M) df:M → Ghf:f ∈ DimSet (M → G) (dim G * d⁻¹)⊢ ((u1.dimScale u2) (dim G) * (u2.dimScale u1) d * (u2.dimScale u1) (dim G * d⁻¹)) • ∫ (x : M), f x ∂μ =
  ((u1.dimScale u2) (dim G) * (u2.dimScale u1) (dim G) * ((u2.dimScale u1) d * (u1.dimScale u2) d)) • ∫ (x : M), f x ∂μ
      congr 1e_aM:Typeinst✝⁷:NormedAddCommGroup Minst✝⁶:NormedSpace ℝ Minst✝⁵:HasDim Minst✝⁴:MeasurableSpace Minst✝³:MeasurableConstSMul ℝ MG:Typeinst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace ℝ Ginst✝:HasDim Gd:Dimension LTMCTDimensionBaseu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesμ:Measure Mhμ:μ ∈ DimSet (Measure M) df:M → Ghf:f ∈ DimSet (M → G) (dim G * d⁻¹)⊢ (u1.dimScale u2) (dim G) * (u2.dimScale u1) d * (u2.dimScale u1) (dim G * d⁻¹) =
  (u1.dimScale u2) (dim G) * (u2.dimScale u1) (dim G) * ((u2.dimScale u1) d * (u1.dimScale u2) d)
      conv_lhs => simp only [map_mul]M:Typeinst✝⁷:NormedAddCommGroup Minst✝⁶:NormedSpace ℝ Minst✝⁵:HasDim Minst✝⁴:MeasurableSpace Minst✝³:MeasurableConstSMul ℝ MG:Typeinst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace ℝ Ginst✝:HasDim Gd:Dimension LTMCTDimensionBaseu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesμ:Measure Mhμ:μ ∈ DimSet (Measure M) df:M → Ghf:f ∈ DimSet (M → G) (dim G * d⁻¹)| (u1.dimScale u2) (dim G) * (u2.dimScale u1) d * ((u2.dimScale u1) (dim G) * (u2.dimScale u1) d⁻¹)
      rw [LTMCTUnitChoices.dimScale_of_inv_eq_swape_aM:Typeinst✝⁷:NormedAddCommGroup Minst✝⁶:NormedSpace ℝ Minst✝⁵:HasDim Minst✝⁴:MeasurableSpace Minst✝³:MeasurableConstSMul ℝ MG:Typeinst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace ℝ Ginst✝:HasDim Gd:Dimension LTMCTDimensionBaseu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesμ:Measure Mhμ:μ ∈ DimSet (Measure M) df:M → Ghf:f ∈ DimSet (M → G) (dim G * d⁻¹)⊢ (u1.dimScale u2) (dim G) * (u2.dimScale u1) d * ((u2.dimScale u1) (dim G) * (u1.dimScale u2) d) =
  (u1.dimScale u2) (dim G) * (u2.dimScale u1) (dim G) * ((u2.dimScale u1) d * (u1.dimScale u2) d)e_aM:Typeinst✝⁷:NormedAddCommGroup Minst✝⁶:NormedSpace ℝ Minst✝⁵:HasDim Minst✝⁴:MeasurableSpace Minst✝³:MeasurableConstSMul ℝ MG:Typeinst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace ℝ Ginst✝:HasDim Gd:Dimension LTMCTDimensionBaseu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesμ:Measure Mhμ:μ ∈ DimSet (Measure M) df:M → Ghf:f ∈ DimSet (M → G) (dim G * d⁻¹)⊢ (u1.dimScale u2) (dim G) * (u2.dimScale u1) d * ((u2.dimScale u1) (dim G) * (u1.dimScale u2) d) =
  (u1.dimScale u2) (dim G) * (u2.dimScale u1) (dim G) * ((u2.dimScale u1) d * (u1.dimScale u2) d)]e_aM:Typeinst✝⁷:NormedAddCommGroup Minst✝⁶:NormedSpace ℝ Minst✝⁵:HasDim Minst✝⁴:MeasurableSpace Minst✝³:MeasurableConstSMul ℝ MG:Typeinst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace ℝ Ginst✝:HasDim Gd:Dimension LTMCTDimensionBaseu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesμ:Measure Mhμ:μ ∈ DimSet (Measure M) df:M → Ghf:f ∈ DimSet (M → G) (dim G * d⁻¹)⊢ (u1.dimScale u2) (dim G) * (u2.dimScale u1) d * ((u2.dimScale u1) (dim G) * (u1.dimScale u2) d) =
  (u1.dimScale u2) (dim G) * (u2.dimScale u1) (dim G) * ((u2.dimScale u1) d * (u1.dimScale u2) d)
      ringAll goals completed! 🐙
    _ = ∫ (x : M), f x ∂ μ := byM:Typeinst✝⁷:NormedAddCommGroup Minst✝⁶:NormedSpace ℝ Minst✝⁵:HasDim Minst✝⁴:MeasurableSpace Minst✝³:MeasurableConstSMul ℝ MG:Typeinst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace ℝ Ginst✝:HasDim Gd:Dimension LTMCTDimensionBaseu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesμ:Measure Mhμ:μ ∈ DimSet (Measure M) df:M → Ghf:f ∈ DimSet (M → G) (dim G * d⁻¹)⊢ ((u1.dimScale u2) (dim G) * (u2.dimScale u1) (dim G) * ((u2.dimScale u1) d * (u1.dimScale u2) d)) • ∫ (x : M), f x ∂μ =
  ∫ (x : M), f x ∂μ simpAll goals completed! 🐙