OAI/Analysis/Mahler/LogJet.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SymmetricMahler.projectD line 17

   Source documentation

   Real or imaginary projection of a complex first derivative.

   def projectD (p : ℂ →L[ℝ] ℝ) : (E →L[ℂ] ℂ) →L[ℝ] (E →L[ℝ] ℝ) :=
   …

2. def OAI.SymmetricMahler.projectD2 line 21

   Source documentation

   Explicit restriction in both arguments of a nested complex derivative.

   def projectD2 (p : ℂ →L[ℝ] ℝ) (B : E →L[ℂ] (E →L[ℂ] ℂ)) :
       E →L[ℝ] (E →L[ℝ] ℝ) := (projectD p).comp (B.restrictScalars ℝ)

   Mentions: OAI.SymmetricMahler.projectD

3. lemma OAI.SymmetricMahler.hasFDerivAt_project line 24
4. lemma OAI.SymmetricMahler.hasFDerivAt_projectD line 29
5. def OAI.SymmetricMahler.squareD line 37

   Source documentation

   The square and its first two derivatives, with the second derivative as an iterated continuous real linear map.

   def squareD (v : ℝ) (A : E →L[ℝ] ℝ) := (2*v) • A

6. def OAI.SymmetricMahler.squareD2 line 39
7. lemma OAI.SymmetricMahler.hasFDerivAt_square line 43
8. lemma OAI.SymmetricMahler.hasFDerivAt_squareD line 48