OAI/Analysis/Mahler/RescaledMassMap.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MahlerRescaling.leadingComponent line 12
2. lemma OAI.MahlerRescaling.leadingComponent_differentiable line 16
3. lemma OAI.MahlerRescaling.homogeneous_eval_scale line 22
4. lemma OAI.MahlerRescaling.leadingComponent_scale line 34
5. lemma OAI.MahlerRescaling.leadingComponent_zero line 40
6. def OAI.MahlerRescaling.taylorRemainder line 44
7. lemma OAI.MahlerRescaling.source_remainder_bound line 48
8. lemma OAI.MahlerRescaling.source_remainder_zero line 57
9. theorem OAI.MahlerRescaling.source_remainder_uniform_C2 line 65

   Source documentation

   The literal mass hypotheses imply uniform convergence of every remainder jet through order two on a fixed closed neighborhood of the unit sphere.

   theorem source_remainder_uniform_C2 {U : Set (Mahler.ComplexEuclidean n)}
       {f : Fin N → Mahler.ComplexEuclidean n → ℂ} {G : Fin N → MvPolynomial (Fin n) ℂ}
       (h : Mahler.MassHypotheses n N m U f G) (j : Fin N) :
       TendstoUniformlyOn (fun ε : ℝ => rescale (taylorRemainder f G j) m ε) (fun _ => 0)
         (𝓝[>] 0) (closedBall 0 2) ∧
       TendstoUniformlyOn (fun ε : ℝ => fderiv ℂ (rescale (taylorRemainder f G j) m ε))
         (fun _ => 0) (𝓝[>] 0) (closedBall 0 2) ∧
       TendstoUniformlyOn (fun ε : ℝ => fderiv ℂ (fderiv ℂ (rescale (taylorRemainder f G j) m ε)))
         (fun _ => 0) (𝓝[>] 0) (closedBall 0 2) := by
   …

   Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.MassHypotheses, OAI.MahlerRescaling.rescale, OAI.MahlerRescaling.taylorRemainder

10. lemma OAI.MahlerRescaling.rescaled_source_remainder line 78