SourceLogC2.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.MahlerRescaling.rescaledLogEnergy line 15
Source documentation
The exact logarithm in the rescaled mass argument.
```
def rescaledLogEnergy (f : Fin N → Mahler.ComplexEuclidean n → ℂ) (m : ℕ)
    (ε : ℝ) (z : Mahler.ComplexEuclidean n) : ℝ :=
…
```
Mentions: OAI.Mahler.ComplexEuclidean
def OAI.MahlerRescaling.leadingLogEnergy line 19
lemma OAI.MahlerRescaling.rescaled_sumNormSq_eq_tau line 25
Source documentation
The norm sum is the rescaled tau, with no normalization factor omitted. This identity also holds at epsilon=0.
```
lemma rescaled_sumNormSq_eq_tau (ε : ℝ) (z : Mahler.ComplexEuclidean n) :
    (∑ j, Complex.normSq (rescale (f j) m ε z)) =
      (ε^(2*m))⁻¹ * Mahler.tau f (ε • z) := by
…
```
Mentions: OAI.Mahler.ComplexEuclidean, OAI.MahlerRescaling.rescale, OAI.Mahler.tau
lemma OAI.MahlerRescaling.rescaledLogEnergy_eq_log_tau line 31
theorem OAI.MahlerRescaling.source_rescaling_log_uniform_C2 line 35

theorem OAI.MahlerRescaling.source_rescaling_log_tau_uniform_C2 line 71

Source documentation

The logarithmic jet limit expressed through the rescaled tau.

theorem source_rescaling_log_tau_uniform_C2 (h : Mahler.MassHypotheses n N m U f G) :
    (∃ c : ℝ, 0 < c ∧ ∀ᶠ ε in 𝓝[>] (0 : ℝ),
      ∀ z ∈ SymmetricMahler.logCompactAnnulus n,
        c ≤ (ε^(2*m))⁻¹ * Mahler.tau f (ε • z)) ∧
    TendstoUniformlyOn (fun ε z => Real.log ((ε^(2*m))⁻¹ * Mahler.tau f (ε • z)))
      (fun z => Real.log (Mahler.tau (leadingComponent G) z))
      (𝓝[>] 0) (SymmetricMahler.logCompactAnnulus n) ∧
    TendstoUniformlyOn (fun ε => fderiv ℝ (fun z => Real.log ((ε^(2*m))⁻¹ * Mahler.tau f (ε • z))))
      (fderiv ℝ (fun z => Real.log (Mahler.tau (leadingComponent G) z)))
      (𝓝[>] 0) (SymmetricMahler.logCompactAnnulus n) ∧
    TendstoUniformlyOn
      (fun ε => fderiv ℝ (fderiv ℝ (fun z => Real.log ((ε^(2*m))⁻¹ * Mahler.tau f (ε • z)))))
…

Mentions: OAI.Mahler.MassHypotheses, OAI.SymmetricMahler.logCompactAnnulus, OAI.Mahler.tau, OAI.MahlerRescaling.leadingComponent