MarkedDisplacements.lean`

29 declarations, 0 contain sorry, 0 declared as axioms

Nonintegral displacements in global and marked theta products; Assembly of marked smooth cubic configurations; Distinct torus configurations at a fixed period

def OAI.Nagata.W06.TorusConfiguration.markedPi line 21
Source documentation
The actual finite product of the nine actual infinite theta products.
```
def markedPi (τ : ℝ) (xi : Fin 9 → ℝ) (z : ℂ) : ℂ :=
…
```
def OAI.Nagata.W06.TorusConfiguration.piMultiplier line 25
Source documentation
Literal unit-valued multiplier of the degree-nine marked theta product.
```
def piMultiplier (τ : ℝ) (xi : Fin 9 → ℝ) : ℂˣ := ∏ i, -(rayPoint τ (xi i))
```
theorem OAI.Nagata.W06.TorusConfiguration.piMultiplier_coe line 27
theorem OAI.Nagata.W06.TorusConfiguration.complexPeriod_norm_lt_one line 31
theorem OAI.Nagata.W06.TorusConfiguration.positivePeriod_free line 34

theorem OAI.Nagata.W06.TorusConfiguration.markedPi_eq_markedThetaSection line 40

Source documentation

The scalar product is exactly the already-proved genuine holomorphic section on the cover.

theorem markedPi_eq_markedThetaSection {τ : ℝ} (hτ : 0 < τ) (hτ1 : τ < 1)
    (xi : Fin 9 → ℝ) (z : ℂˣ) :
    markedPi τ xi (z : ℂ) =
      (Nagata.W08.markedThetaSection (complexPeriod_norm_lt_one hτ hτ1)
        (Complex.ofReal_ne_zero.mpr (ne_of_gt hτ))
        (fun i => (rayPoint τ (xi i) : ℂ)) (fun _ => Units.ne_zero _)).val (z : ℂ) := by
…

Mentions: OAI.Nagata.W06.TorusConfiguration.markedPi, OAI.Nagata.W08.markedThetaSection, OAI.Nagata.W06.TorusConfiguration.complexPeriod_norm_lt_one

theorem OAI.Nagata.W06.TorusConfiguration.markedPi_zero_fixed line 50

theorem OAI.Nagata.W06.TorusConfiguration.markedPi_ne_zero_of_torus_avoidance line 58

Source documentation

Noncollision with the nine quotient points implies nonvanishing of the actual Pi.

theorem markedPi_ne_zero_of_torus_avoidance {τ : ℝ} (hτ : 0 < τ) (hτ1 : τ < 1)
    (xi : Fin 9 → ℝ) (z : ℂˣ)
    (havoid : ∀ i, torusPointMk (positivePeriod τ hτ) z ≠
      torusPointMk (positivePeriod τ hτ) (rayPoint τ (xi i))) :
    markedPi τ xi (z : ℂ) ≠ 0 := by
…

Mentions: OAI.Nagata.W06.TorusConfiguration.markedPi

theorem OAI.Nagata.W06.TorusConfiguration.moving_avoids_fixed_of_tuple_injective line 73
theorem OAI.Nagata.W06.TorusConfiguration.markedPi_ne_zero_moving line 86
def OAI.Nagata.W06.TorusConfiguration.displacementScalar line 94
Source documentation
The literal finite source displacement scalars: nine zeros, followed by Pi(z_j).
```
def displacementScalar (τ x0 : ℝ) (xi : Fin 9 → ℝ) {q : ℕ} (ξ : Fin q → ℂ) :
    Fin (9 + q) → ℂ :=
…
```
theorem OAI.Nagata.W06.TorusConfiguration.displacementScalar_left line 100
theorem OAI.Nagata.W06.TorusConfiguration.displacementScalar_right line 105
def OAI.Nagata.W06.TorusConfiguration.normalDisplacement line 113
Source documentation
The displacement at each actual tuple point, in the actual normal multiplier fibre D(9,L³). L is the degree-three multiplier; the cubic/normal-bundle identification is a separate input.
```
def normalDisplacement (τ : ℝ) (hτ : 0 < τ) (L : ℂˣ) (x0 : ℝ) (xi : Fin 9 → ℝ)
    {q : ℕ} (ξ : Fin q → ℂ) (t : Fin (9 + q)) :
    QuotientFibre (positivePeriod τ hτ) (L ^ 3) 9 (torusTuple τ hτ x0 xi ξ t) :=
…
```
Mentions: OAI.Nagata.W06.TorusConfiguration.QuotientFibre, OAI.Nagata.W06.TorusConfiguration.torusTuple
theorem OAI.Nagata.W06.TorusConfiguration.normalDisplacement_left line 119
theorem OAI.Nagata.W06.TorusConfiguration.normalDisplacement_right line 126
theorem OAI.Nagata.W06.TorusConfiguration.movingDisplacement_Pi_times_one line 136
Source documentation
Over every selected moving lift, the actual source-fibre scalar-one vector is sent to the actual target-fibre displacement by multiplication with the actual Pi.
```
theorem movingDisplacement_Pi_times_one {τ : ℝ} (hτ : 0 < τ) (hτ1 : τ < 1)
    (L : ℂˣ) (xi : Fin 9 → ℝ) (z : ℂˣ) :
    fibreScaleAtLift (positivePeriod τ hτ) (L ^ 3 / piMultiplier τ xi) (L ^ 3) 0 9
      (positivePeriod_free hτ hτ1) z (markedPi τ xi (z : ℂ))
      (fibreRepresentative (positivePeriod τ hτ) (L ^ 3 / piMultiplier τ xi) 0 z 1) =
      fibreRepresentative (positivePeriod τ hτ) (L ^ 3) 9 z (markedPi τ xi (z : ℂ)) :=
…
```
Mentions: OAI.Nagata.W06.TorusConfiguration.fibreScaleAtLift, OAI.Nagata.W06.TorusConfiguration.piMultiplier, OAI.Nagata.W06.TorusConfiguration.positivePeriod_free, OAI.Nagata.W06.TorusConfiguration.markedPi, OAI.Nagata.W06.TorusConfiguration.fibreRepresentative

theorem OAI.Nagata.W06.TorusConfiguration.movingDisplacement_ne_zero line 145

Source documentation

Every moving displacement is nonzero in its actual quotient fibre.

theorem movingDisplacement_ne_zero {τ : ℝ} (hτ : 0 < τ) (hτ1 : τ < 1)
    (L : ℂˣ) (x0 : ℝ) (xi : Fin 9 → ℝ) {q : ℕ} (ξ : Fin q → ℂ)
    (hinj : Function.Injective (torusTuple τ hτ x0 xi ξ)) (j : Fin q) :
    fibreRepresentative (positivePeriod τ hτ) (L ^ 3) 9 (chartPoint τ x0 (ξ j))
        (markedPi τ xi (chartPoint τ x0 (ξ j) : ℂ)) ≠
      fibreRepresentative (positivePeriod τ hτ) (L ^ 3) 9 (chartPoint τ x0 (ξ j)) 0 :=
…

Mentions: OAI.Nagata.W06.TorusConfiguration.torusTuple, OAI.Nagata.W06.TorusConfiguration.fibreRepresentative, OAI.Nagata.W06.TorusConfiguration.markedPi

def OAI.Nagata.W06.TorusConfiguration.piSection line 168
Source documentation
The genuine holomorphic marked section, typed with the literal unit multiplier Q.
```
def piSection {τ : ℝ} (hτ : 0 < τ) (hτ1 : τ < 1) (xi : Fin 9 → ℝ) :
    Nagata.W08.automorphicSections (positivePeriod τ hτ : ℂ) 9 (piMultiplier τ xi : ℂ) :=
…
```
Mentions: OAI.Nagata.W08.automorphicSections, OAI.Nagata.W06.TorusConfiguration.piMultiplier
theorem OAI.Nagata.W06.TorusConfiguration.piSection_apply line 179

def OAI.Nagata.W06.TorusConfiguration.quotientParameterCast line 184

Source documentation

Change only the parameter names of a genuine multiplier quotient.

def quotientParameterCast {τ γ γ' : ℂˣ} {n n' : ℤ} (hγ : γ = γ') (hn : n = n') :
    MultiplierQuotient τ γ n → MultiplierQuotient τ γ' n' := by
…

theorem OAI.Nagata.W06.TorusConfiguration.quotientParameterCast_mk line 188
def OAI.Nagata.W06.TorusConfiguration.piQuotientMap line 193
theorem OAI.Nagata.W06.TorusConfiguration.piQuotientMap_mk line 200

theorem OAI.Nagata.W06.TorusConfiguration.piQuotientMap_projection line 208

Source documentation

The global morphism preserves the actual base point.

theorem piQuotientMap_projection {τ : ℝ} (hτ : 0 < τ) (hτ1 : τ < 1)
    (L : ℂˣ) (xi : Fin 9 → ℝ)
    (w : MultiplierQuotient (positivePeriod τ hτ) (L ^ 3 / piMultiplier τ xi) 0) :
    multiplierQuotientProjection (positivePeriod τ hτ) (L ^ 3) 9
        (piQuotientMap hτ hτ1 L xi w) =
      multiplierQuotientProjection (positivePeriod τ hτ) (L ^ 3 / piMultiplier τ xi) 0 w := by
…

Mentions: OAI.Nagata.W06.TorusConfiguration.piMultiplier, OAI.Nagata.W06.TorusConfiguration.piQuotientMap

theorem OAI.Nagata.W06.TorusConfiguration.normalDisplacement_eq_globalPi line 221
Source documentation
The complete literal zero/Pi displacement list is induced by one global map, evaluated on scalar-one representatives at every chosen covering lift.
```
theorem normalDisplacement_eq_globalPi {τ : ℝ} (hτ : 0 < τ) (hτ1 : τ < 1)
    (L : ℂˣ) (x0 : ℝ) (xi : Fin 9 → ℝ) {q : ℕ} (ξ : Fin q → ℂ) (t : Fin (9 + q)) :
    (normalDisplacement τ hτ L x0 xi ξ t).val =
      piQuotientMap hτ hτ1 L xi (Quotient.mk _ (coverTuple τ x0 xi ξ t, (1 : ℂ))) := by
…
```
Mentions: OAI.Nagata.W06.TorusConfiguration.normalDisplacement, OAI.Nagata.W06.TorusConfiguration.piQuotientMap, OAI.Nagata.W06.TorusConfiguration.coverTuple

theorem OAI.Nagata.W06.TorusConfiguration.exists_eventual_sourceMarkedAssembly line 249

Source documentation

Explicit source exponents, one common disk, all finite collision configurations, and nonzero actual Pi values at every moving point, uniformly for small periods.

theorem exists_eventual_sourceMarkedAssembly {Δ : ℝ} (hΔ : 0 < Δ) (hhalf : Δ < 1 / 2) :
    ∃ R : ℝ, 0 < R ∧ R < Real.pi / 2 ∧
      (∀ q i, Tendsto (fun n => Nagata.W20.collisionCenters q R n i) atTop (𝓝 0)) ∧
      ∀ᶠ τ : ℝ in 𝓝[>] 0, 0 < τ ∧ τ < 1 ∧
        ∀ (hτ : 0 < τ) (q n : ℕ),
          Function.Injective (torusTuple τ hτ (1 / 2) (markedExponent Δ)
            (Nagata.W20.collisionCenters q R n)) ∧
          ∀ j : Fin q, markedPi τ (markedExponent Δ)
            (chartPoint τ (1 / 2) (Nagata.W20.collisionCenters q R n j) : ℂ) ≠ 0 := by
…

Mentions: OAI.Nagata.W20.collisionCenters, OAI.Nagata.W06.TorusConfiguration.torusTuple, OAI.Nagata.W06.markedExponent, OAI.Nagata.W06.TorusConfiguration.markedPi

theorem OAI.Nagata.W06.TorusConfiguration.exists_disk_for_fixed_period line 283

Source documentation

Every fixed genuine period admits a disk for all finite moving configurations.

theorem exists_disk_for_fixed_period {τ : ℝ} (hτ : 0 < τ) (hτ1 : τ < 1)
    (xi : Fin 9 → ℝ) (hxi : Function.Injective xi)
    (hxi_bounds : ∀ i, 0 < xi i ∧ xi i < 1 / 2) :
    ∃ R : ℝ, 0 < R ∧ ∀ (q : ℕ) (ξ : Fin q → ℂ),
      Function.Injective ξ → (∀ j, ‖ξ j‖ < R) →
      Function.Injective (torusTuple τ hτ (1 / 2) xi ξ) ∧
        ∀ j, markedPi τ xi (chartPoint τ (1 / 2) (ξ j) : ℂ) ≠ 0 := by
…

Mentions: OAI.Nagata.W06.TorusConfiguration.torusTuple, OAI.Nagata.W06.TorusConfiguration.markedPi

theorem OAI.Nagata.W06.TorusConfiguration.sourceMarkedAssembly_for_every_period line 314

Source documentation

Exact source marked parameters work for every 0<τ<1, with q arbitrary.

theorem sourceMarkedAssembly_for_every_period {Δ τ : ℝ}
    (hΔ : 0 < Δ) (hhalf : Δ < 1 / 2) (hτ : 0 < τ) (hτ1 : τ < 1) :
    ∃ R : ℝ, 0 < R ∧ ∀ (q : ℕ) (ξ : Fin q → ℂ),
      Function.Injective ξ → (∀ j, ‖ξ j‖ < R) →
      Function.Injective (torusTuple τ hτ (1 / 2) (markedExponent Δ) ξ) ∧
        ∀ j, markedPi τ (markedExponent Δ) (chartPoint τ (1 / 2) (ξ j) : ℂ) ≠ 0 :=
…

Mentions: OAI.Nagata.W06.TorusConfiguration.torusTuple, OAI.Nagata.W06.markedExponent, OAI.Nagata.W06.TorusConfiguration.markedPi