Documentation

LeanPool.LocalComplexGeometry.WPTBridge.DivisionCore

Sequence-level Weierstrass division bridge #

This file packages the analytic quotient and remainder sequence operators for prepared divisors so the local complex-geometry development can reuse them.

source
noncomputable def LocalComplexGeometry.WPTBridge.DivisionCore.divisionInput {n d : ℕ} (p : FormalMultilinearSeries ℂ (ClassicalComplexWPT.Ambient n) ℂ) (r : NNReal) (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (z : ClassicalComplexWPT.Base n) :
↥ClassicalComplexWPT.L1Sequence × ↥ClassicalComplexWPT.L1Sequence

Analytic divisor-tail/dividend input for WPT's total sequence division maps.

Equations
Instances For
    source
    noncomputable def LocalComplexGeometry.WPTBridge.DivisionCore.quotientSeq {n d : ℕ} (p : FormalMultilinearSeries ℂ (ClassicalComplexWPT.Ambient n) ℂ) (r : NNReal) (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (z : ClassicalComplexWPT.Base n) :
    ↥ClassicalComplexWPT.L1Sequence

    Sequence quotient supplied by the pinned WPT division operator.

    Equations
    Instances For
      source
      noncomputable def LocalComplexGeometry.WPTBridge.DivisionCore.remainderSeq {n d : ℕ} (p : FormalMultilinearSeries ℂ (ClassicalComplexWPT.Ambient n) ℂ) (r : NNReal) (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (z : ClassicalComplexWPT.Base n) :
      ↥ClassicalComplexWPT.L1Sequence

      Sequence remainder supplied by the pinned WPT division operator.

      Equations
      Instances For
        source
        theorem LocalComplexGeometry.WPTBridge.DivisionCore.preparedTailSeq_zero {n d : ℕ} (r : NNReal) (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha0 : ∀ (i : Fin d), a i 0 = 0) :
        ClassicalComplexWPT.preparedTailSeq r d a 0 = 0
        source
        theorem LocalComplexGeometry.WPTBridge.DivisionCore.norm_divisionInput_fst_zero_lt_one {n d : ℕ} (r : NNReal) (p : FormalMultilinearSeries ℂ (ClassicalComplexWPT.Ambient n) ℂ) (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha0 : ∀ (i : Fin d), a i 0 = 0) :
        ‖(divisionInput p r a 0).1‖ < 1
        source
        theorem LocalComplexGeometry.WPTBridge.DivisionCore.analyticAt_divisionInput {n d : ℕ} (p : FormalMultilinearSeries ℂ (ClassicalComplexWPT.Ambient n) ℂ) (r : NNReal) (hrp : ↑r < p.radius) (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) :
        AnalyticAt ℂ (divisionInput p r a) 0
        source
        theorem LocalComplexGeometry.WPTBridge.DivisionCore.analyticAt_quotientSeq {n d : ℕ} (p : FormalMultilinearSeries ℂ (ClassicalComplexWPT.Ambient n) ℂ) (r : NNReal) (hrp : ↑r < p.radius) (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) :
        AnalyticAt ℂ (quotientSeq p r a) 0
        source
        theorem LocalComplexGeometry.WPTBridge.DivisionCore.analyticAt_remainderSeq {n d : ℕ} (p : FormalMultilinearSeries ℂ (ClassicalComplexWPT.Ambient n) ℂ) (r : NNReal) (hrp : ↑r < p.radius) (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) :
        AnalyticAt ℂ (remainderSeq p r a) 0
        source
        theorem LocalComplexGeometry.WPTBridge.DivisionCore.quotient_remainderSeq_unique {n d : ℕ} (p : FormalMultilinearSeries ℂ (ClassicalComplexWPT.Ambient n) ℂ) (r : NNReal) (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (z : ClassicalComplexWPT.Base n) (hsmall : ‖ClassicalComplexWPT.preparedTailSeq r d a z‖ < 1) (q remainder : ↥ClassicalComplexWPT.L1Sequence) (hfactor : (ClassicalComplexWPT.weightedCoefficientSeries p r).sum z = ClassicalComplexWPT.seqLowShift d q + ClassicalComplexWPT.convolution q (ClassicalComplexWPT.preparedTailSeq r d a z) + remainder) (hsupport : ClassicalComplexWPT.seqHighShift d remainder = 0) :
        q = quotientSeq p r a z ∧ remainder = remainderSeq p r a z

        Pointwise uniqueness of the sequence quotient and low-degree remainder.