OAI/Analysis/Mahler/RawCoefficientDerivative.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Mahler.rawCoefficientDerivative line 13
2. lemma OAI.Mahler.rawCoefficientDerivative_apply line 20
3. def OAI.Mahler.HasRawFDerivAt line 26

   Source documentation

   A coefficientwise derivative records actual HasFDerivAt proofs for all tuples. It adds no differentiability or exterior-calculus assumptions.

   def HasRawFDerivAt (a : E → MultilinearMap ℝ (fun _ : ι => E) ℂ)
       (D : E →ₗ[ℝ] MultilinearMap ℝ (fun _ : ι => E) ℂ) (x : E) : Prop :=
   …

4. theorem OAI.Mahler.HasRawFDerivAt.product line 31
5. theorem OAI.Mahler.HasRawFDerivAt.power line 46