SourceRescaling.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.MahlerRescaling.source_rescaling_C2_bound line 15

Source documentation

The rescaled functions themselves, with their actual Frechet derivatives, converge at order epsilon to the stated homogeneous leading polynomial.

theorem source_rescaling_C2_bound (h : Mahler.MassHypotheses n N m U f G) (j : Fin N) :
    ∃ C > 0, ∃ δ > 0, ∀ ε : ℝ, 0 < ε → ε < δ →
      DifferentiableOn ℂ (rescale (f j) m ε) (ball 0 4) ∧
      ∀ z ∈ closedBall (0 : Mahler.ComplexEuclidean n) 2,
        ‖rescale (f j) m ε z-leadingComponent G j z‖ ≤ C*ε ∧
        ‖fderiv ℂ (rescale (f j) m ε) z-fderiv ℂ (leadingComponent G j) z‖ ≤ C*ε ∧
        ‖fderiv ℂ (fderiv ℂ (rescale (f j) m ε)) z-
          fderiv ℂ (fderiv ℂ (leadingComponent G j)) z‖ ≤ C*ε := by
…

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

theorem OAI.MahlerRescaling.source_rescaling_uniform_C2 line 62

Source documentation

The exact C² convergence used at the small-sphere limit, expressed in uniform convergence of the function and its first two complex derivatives.

theorem source_rescaling_uniform_C2 (h : Mahler.MassHypotheses n N m U f G) (j : Fin N) :
    TendstoUniformlyOn (fun ε : ℝ => rescale (f j) m ε) (leadingComponent G j)
      (𝓝[>] 0) (closedBall 0 2) ∧
    TendstoUniformlyOn (fun ε : ℝ => fderiv ℂ (rescale (f j) m ε))
      (fderiv ℂ (leadingComponent G j)) (𝓝[>] 0) (closedBall 0 2) ∧
    TendstoUniformlyOn (fun ε : ℝ => fderiv ℂ (fderiv ℂ (rescale (f j) m ε)))
      (fderiv ℂ (fderiv ℂ (leadingComponent G j))) (𝓝[>] 0) (closedBall 0 2) := by
…

Mentions: OAI.Mahler.MassHypotheses, OAI.MahlerRescaling.rescale, OAI.MahlerRescaling.leadingComponent