CoordinateMinorPermutation.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Reordering an actual nonzero minor into the sliced coordinates

theorem OAI.PolycyclicRecognition.exists_fin_equiv_extending_injection line 16
def OAI.PolycyclicRecognition.reindexParameters line 29
Source documentation
This map permutes coordinates, preserving both the cube and Lebesgue measure.
```
def reindexParameters {l m : ℕ} (e : Fin l ≃ Fin m) :
    (Fin l → ℝ) →L[ℝ] (Fin m → ℝ) :=
…
```
theorem OAI.PolycyclicRecognition.reindexParameters_apply line 33
theorem OAI.PolycyclicRecognition.reindexParameters_apply_equiv line 36
theorem OAI.PolycyclicRecognition.reindexParameters_norm line 39
theorem OAI.PolycyclicRecognition.measurePreserving_reindexParameters line 45
theorem OAI.PolycyclicRecognition.HasPolynomialFormula.reindex line 52
theorem OAI.PolycyclicRecognition.reindexParameters_single line 63

theorem OAI.PolycyclicRecognition.det_reindexed_slice line 71

Source documentation

The selected column determinant is the derivative determinant after reordering.

theorem det_reindexed_slice {n k m : ℕ} (e : Fin (n + k) ≃ Fin m)
    (f : (Fin m → ℝ) → (Fin n → ℝ)) (v : Fin n → ℝ) (z : Fin k → ℝ)
    (hf : DifferentiableAt ℝ f (reindexParameters e (Fin.append v z))) :
    (fderiv ℝ (fun w => f (reindexParameters e (Fin.append w z))) v).det =
      (Matrix.of fun i j => fderiv ℝ f (reindexParameters e (Fin.append v z))
        (Pi.single (e (Fin.castAdd k j)) 1) i).det := by
…

Mentions: OAI.PolycyclicRecognition.reindexParameters