OAI/Analysis/Mahler/SpecialLeadingTerm.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SymmetricMahler.inverseLinearCoefficient line 14
  2. lemma OAI.SymmetricMahler.inverseLinearCoefficient_ne_zero line 16
  3. lemma OAI.SymmetricMahler.analyticAt_inverseF_zero line 19
  4. lemma OAI.SymmetricMahler.analyticAt_inverseF_dslope line 22
  5. lemma OAI.SymmetricMahler.inverseF_factor line 26
  6. theorem OAI.SymmetricMahler.inverseF_power_leading line 31

    Source documentation

    The exact univariate power has its asserted degree-m leading term and an order-(m+1) remainder. The divided difference handles the origin.

    theorem inverseF_power_leading (m : ā„•) :
    (fun w : ā„‚ => inverseF w^m-(inverseLinearCoefficient*w)^m) =O[š“ 0]
      (fun w : ā„‚ => ā€–wā€–^(m+1)) := by
ā€¦

    Mentions: OAI.SymmetricMahler.inverseLinearCoefficient

  7. def OAI.SymmetricMahler.specialLeadingMap line 44
  8. def OAI.SymmetricMahler.specialLeadingPolynomial line 47
  9. lemma OAI.SymmetricMahler.specialLeadingPolynomial_eval line 51
  10. lemma OAI.SymmetricMahler.specialLeadingPolynomial_homogeneous line 56
  11. theorem OAI.SymmetricMahler.specialLeadingMap_eq_zero_iff line 64

    Source documentation

    The leading homogeneous map is nonzero away from zero whenever the rows have full rank. This includes every coordinate, rather than a scalar slice.

    theorem specialLeadingMap_eq_zero_iff (A : Matrix (Fin N) (Fin n) ā„)
    (hA : Function.Injective (measurement A)) {m : ā„•} (hm : 0 < m)
    (z : Fin n ā†’ ā„‚) : specialLeadingMap A m z = 0 ā†” z = 0 := by
ā€¦

    Mentions: OAI.SymmetricMahler.measurement, OAI.SymmetricMahler.specialLeadingMap

  12. theorem OAI.SymmetricMahler.specialMap_leading_remainder line 82

    Source documentation

    The special holomorphic map has the homogeneous leading map, with a norm-controlled order-(m+1) error in all complex variables.

    theorem specialMap_leading_remainder (A : Matrix (Fin N) (Fin n) ā„) (m : ā„•) :
    (fun z : Fin n ā†’ ā„‚ => specialMap A m z-specialLeadingMap A m z) =O[š“ 0]
      (fun z : Fin n ā†’ ā„‚ => ā€–zā€–^(m+1)) := by
ā€¦

    Mentions: OAI.SymmetricMahler.specialMap, OAI.SymmetricMahler.specialLeadingMap