ComplexCoordinates.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

def OAI.MahlerStokes.interleavedEuclidean line 14
Source documentation
Interleaved real coordinates: index 2i is real and index 2i+1 imaginary.
```
def interleavedEuclidean (n : ℕ) :
    EuclideanSpace ℝ (Fin (n*2)) ≃ₗᵢ[ℝ] EuclideanSpace ℂ (Fin n) where
…
```
def OAI.MahlerStokes.complexCoordinates line 41
Source documentation
The same coordinate map on the ordinary Pi space used by the Stokes integrals.
```
def complexCoordinates (n : ℕ) :
    (Fin (n*2) → ℝ) ≃L[ℝ] EuclideanSpace ℂ (Fin n) :=
…
```
lemma OAI.MahlerStokes.complexCoordinates_apply line 46
theorem OAI.MahlerStokes.measurePreserving_complexCoordinates line 50
Source documentation
Euclidean volume is transported with factor exactly one.
```
theorem measurePreserving_complexCoordinates (n : ℕ) :
    MeasurePreserving (complexCoordinates n) := by
…
```
Mentions: OAI.MahlerStokes.complexCoordinates
theorem OAI.MahlerStokes.norm_complexCoordinates_sq line 56
Source documentation
The coordinate squared radius is exactly the complex Euclidean squared norm.
```
theorem norm_complexCoordinates_sq (n : ℕ) (x : Fin (n*2) → ℝ) :
    ‖complexCoordinates n x‖^2 = radiusSq x := by
…
```
Mentions: OAI.MahlerStokes.complexCoordinates, OAI.MahlerStokes.radiusSq
theorem OAI.MahlerStokes.complexCoordinates_basis line 63
Source documentation
The coordinate map sends the ordered real basis to x_i,y_i without a sign or scale change.
```
theorem complexCoordinates_basis (n : ℕ) (i : Fin n) (b : Fin 2) :
    complexCoordinates n (Pi.single (finProdFinEquiv (i,b)) 1) =
      EuclideanSpace.single i (if b = 0 then 1 else Complex.I) := by
…
```
Mentions: OAI.MahlerStokes.complexCoordinates
theorem OAI.MahlerStokes.interleavedIndex_val line 74

theorem OAI.MahlerStokes.setIntegral_complexCoordinates line 80

Source documentation

Ordinary real density integrals in the explicit interleaved coordinates.

theorem setIntegral_complexCoordinates (n : ℕ) (S : Set (EuclideanSpace ℂ (Fin n)))
    (f : EuclideanSpace ℂ (Fin n) → ℝ) :
    (∫ x in (complexCoordinates n) ⁻¹' S, f (complexCoordinates n x)) = ∫ z in S, f z :=
…

Mentions: OAI.MahlerStokes.complexCoordinates

theorem OAI.MahlerStokes.setLIntegral_complexCoordinates line 87

Source documentation

Nonnegative mass integrals transport even when the mass is infinite.

theorem setLIntegral_complexCoordinates (n : ℕ) (S : Set (EuclideanSpace ℂ (Fin n)))
    (f : EuclideanSpace ℂ (Fin n) → ℝ≥0∞) :
    (∫⁻ x in (complexCoordinates n) ⁻¹' S, f (complexCoordinates n x)) = ∫⁻ z in S, f z :=
…

Mentions: OAI.MahlerStokes.complexCoordinates

theorem OAI.MahlerStokes.coordBall_complexCoordinates line 93
theorem OAI.MahlerStokes.coordClosedBall_complexCoordinates line 101