OAI/Analysis/Mahler/Jacobian.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SymmetricMahler.weightedGram line 13
2. lemma OAI.SymmetricMahler.weightedGram_posSemidef line 16
3. lemma OAI.SymmetricMahler.weightedGram_det_nonneg line 21
4. lemma OAI.SymmetricMahler.weightedGram_apply line 25
5. lemma OAI.SymmetricMahler.weightedGram_smul line 32
6. theorem OAI.SymmetricMahler.finite_strip_block_jacobian line 42

   Source documentation

   The x-component is the identity, so arbitrary mixed derivatives in C do not enter the real determinant.

   theorem finite_strip_block_jacobian {n N : ℕ} (A : Matrix (Fin N) (Fin n) ℝ)
       (C : Matrix (Fin n) (Fin n) ℝ) {c : Fin N → ℝ} (hc : ∀ j, 0 ≤ c j)
       {m : ℝ} (hm : 0 < m) :
       |(Matrix.fromBlocks (1 : Matrix (Fin n) (Fin n) ℝ) 0 C
         ((4/(Real.pi*m)) • weightedGram A c)).det| =
         (4/(Real.pi*m))^n*(weightedGram A c).det := by
   …

   Mentions: OAI.SymmetricMahler.weightedGram

7. def OAI.SymmetricMahler.hessianWeight line 52
8. def OAI.SymmetricMahler.verticalWeight line 55
9. lemma OAI.SymmetricMahler.hessianWeight_nonneg line 58
10. lemma OAI.SymmetricMahler.verticalWeight_eq_scaled_hessianWeight line 62
11. theorem OAI.SymmetricMahler.finite_strip_weighted_jacobian line 70

    Source documentation

    The Jacobian coefficient for the weights from h and h'. The only analytic input to this identity is that these are the derivative weights; positivity and the absolute determinant follow.

    theorem finite_strip_weighted_jacobian {n N : ℕ} (A : Matrix (Fin N) (Fin n) ℝ)
        (C : Matrix (Fin n) (Fin n) ℝ) (f d : Fin N → ℂ) {m : ℝ} (hm : 0 < m) :
        |(Matrix.fromBlocks (1 : Matrix (Fin n) (Fin n) ℝ) 0 C
          (weightedGram A (fun j => verticalWeight m (f j) (d j)))).det| =
          (4/(Real.pi*m))^n*(weightedGram A (fun j => hessianWeight m (f j) (d j))).det := by
    …

    Mentions: OAI.SymmetricMahler.weightedGram, OAI.SymmetricMahler.verticalWeight, OAI.SymmetricMahler.hessianWeight