ComplexVolume.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SymmetricMahler.complexEuclideanRealification line 13

Source documentation

Realification with the Euclidean norm on both groups of real coordinates.

noncomputable def complexEuclideanRealification :
    EuclideanSpace ℂ (Fin n) ≃ₗᵢ[ℝ]
      WithLp 2 (EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n)) where
…

theorem OAI.SymmetricMahler.volume_preserving_complexEuclidean_split line 35
Source documentation
Euclidean complex coordinates to separated real coordinates, with exact volume.
```
theorem volume_preserving_complexEuclidean_split :
    MeasurePreserving (fun z : EuclideanSpace ℂ (Fin n) =>
      ((fun i => (z i).re), (fun i => (z i).im))) := by
…
```
theorem OAI.SymmetricMahler.volume_preserving_complex_ofLp line 46
Source documentation
Forgetting the L2 wrapper on complex coordinates preserves standard volume.
```
theorem volume_preserving_complex_ofLp :
    MeasurePreserving (@WithLp.ofLp 2 (Fin n → ℂ)) := by
…
```
theorem OAI.SymmetricMahler.volume_preserving_complex_toLp line 57
Source documentation
The inverse transport from coordinate product volume to Euclidean volume.
```
theorem volume_preserving_complex_toLp :
    MeasurePreserving (@WithLp.toLp 2 (Fin n → ℂ)) :=
…
```

theorem OAI.SymmetricMahler.map_volume_complex_ofLp line 63

Source documentation

Explicit equality of the two measures, with scale factor exactly one.

theorem map_volume_complex_ofLp :
    Measure.map (@WithLp.ofLp 2 (Fin n → ℂ))
      (volume : Measure (EuclideanSpace ℂ (Fin n))) =
        (volume : Measure (Fin n → ℂ)) :=
…

theorem OAI.SymmetricMahler.lintegral_complex_ofLp line 70

Source documentation

Arbitrary nonnegative densities transport without finiteness assumptions.

theorem lintegral_complex_ofLp (g : (Fin n → ℂ) → ℝ≥0∞) :
    (∫⁻ z : EuclideanSpace ℂ (Fin n), g (WithLp.ofLp z)) = ∫⁻ z, g z :=
…

theorem OAI.SymmetricMahler.setLIntegral_complex_ofLp line 77
Source documentation
Restricted density integrals agree on the literal preimage domain. No measurability or finite-mass premise is needed because this is an equivalence.
```
theorem setLIntegral_complex_ofLp (S : Set (Fin n → ℂ))
    (g : (Fin n → ℂ) → ℝ≥0∞) :
    (∫⁻ z in (@WithLp.ofLp 2 (Fin n → ℂ)) ⁻¹' S, g (WithLp.ofLp z)) =
      ∫⁻ z in S, g z :=
…
```

theorem OAI.SymmetricMahler.setLIntegral_complex_toLp line 85

Source documentation

The opposite direction lets a Euclidean density be integrated in coordinates.

theorem setLIntegral_complex_toLp (S : Set (EuclideanSpace ℂ (Fin n)))
    (g : EuclideanSpace ℂ (Fin n) → ℝ≥0∞) :
    (∫⁻ z in (@WithLp.toLp 2 (Fin n → ℂ)) ⁻¹' S, g (WithLp.toLp 2 z)) =
      ∫⁻ z in S, g z :=
…