LogDilation.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Mahler.boundaryForm_congr line 12
def OAI.Mahler.rescaledLog line 21
Source documentation
The rescaling epsilon^(-2m) tau(epsilon z), followed by log.
```
noncomputable def rescaledLog (τ : E → ℝ) (m : ℕ) (r : ℝ) (x : E) : ℂ :=
…
```
lemma OAI.Mahler.rescaledLog_eventually line 25

theorem OAI.Mahler.boundaryForm_rescaledLog line 39

Source documentation

Literal logarithmic rescaling pulls back d^c log tau and every dd^c factor, with no extra scale or orientation sign.

theorem boundaryForm_rescaledLog {τ : E → ℝ} {r : ℝ} {x : E}
    (hr : 0 < r) (hτ : ContinuousAt τ (r • x)) (hp : 0 < τ (r • x))
    (hu : ContDiffAt ℝ 2 (fun y => (Real.log (τ y) : ℂ)) (r • x)) (m k : ℕ) :
    boundaryForm (rescaledLog τ m r) k x =
      (boundaryForm (fun y => (Real.log (τ y) : ℂ)) k (r • x)).compLinearMap
        (realDilation r).toLinearMap := by
…

Mentions: OAI.Mahler.boundaryForm, OAI.Mahler.rescaledLog, OAI.Mahler.realDilation

theorem OAI.Mahler.smallSphereFlux_log_eq line 49

Source documentation

Equality for actual Euclidean surface integrals, before taking a limit.

theorem smallSphereFlux_log_eq {k m : ℕ} {τ : ComplexEuclidean (k+1) → ℝ} {r : ℝ}
    (hr : 0 < r)
    (hτ : ∀ z : sphere (0 : ComplexEuclidean (k+1)) 1,
      ContinuousAt τ (r • (z : ComplexEuclidean (k+1))))
    (hp : ∀ z : sphere (0 : ComplexEuclidean (k+1)) 1,
      0 < τ (r • (z : ComplexEuclidean (k+1))))
    (hu : ∀ z : sphere (0 : ComplexEuclidean (k+1)) 1,
      ContDiffAt ℝ 2 (fun y => (Real.log (τ y) : ℂ)) (r • (z : ComplexEuclidean (k+1)))) :
    smallSphereFlux k (fun y => (Real.log (τ y) : ℂ)) r =
      unitSphereFlux k (rescaledLog τ m r) := by
…

Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.smallSphereFlux, OAI.Mahler.unitSphereFlux, OAI.Mahler.rescaledLog

lemma OAI.Mahler.continuousOn_actualRealComplexJet line 69

theorem OAI.Mahler.smallSphereFlux_log_tendsto line 79

Source documentation

A limit theorem whose analytic inputs are C^2 regularity and uniform first/second log jets on a compact annulus (or any compact set containing the sphere). Transport and integral convergence are conclusions.

theorem smallSphereFlux_log_tendsto {k m : ℕ} {τ : ComplexEuclidean (k+1) → ℝ}
    {v : ComplexEuclidean (k+1) → ℂ} {K : Set (ComplexEuclidean (k+1))}
    (hK : IsCompact K) (hS : sphere (0 : ComplexEuclidean (k+1)) 1 ⊆ K)
    (hv : ∀ x ∈ K, ContDiffAt ℝ 2 v x)
    (hu : ∀ᶠ r in 𝓝[>] (0 : ℝ), ∀ x ∈ K, ContDiffAt ℝ 2 (rescaledLog τ m r) x)
    (hτ : ∀ᶠ r in 𝓝[>] (0 : ℝ), ∀ z : sphere (0 : ComplexEuclidean (k+1)) 1,
      ContinuousAt τ (r • (z : ComplexEuclidean (k+1))))
    (hp : ∀ᶠ r in 𝓝[>] (0 : ℝ), ∀ z : sphere (0 : ComplexEuclidean (k+1)) 1,
      0 < τ (r • (z : ComplexEuclidean (k+1))))
    (hlog : ∀ᶠ r in 𝓝[>] (0 : ℝ), ∀ z : sphere (0 : ComplexEuclidean (k+1)) 1,
      ContDiffAt ℝ 2 (fun y => (Real.log (τ y) : ℂ)) (r • (z : ComplexEuclidean (k+1))))
    (h1 : TendstoUniformlyOn (fun r => fderiv ℝ (rescaledLog τ m r))
…

Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.rescaledLog