OAI/AlgebraicGeometry/PlaneCurves/AnalyticScaling.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Analytic jet composition, normal scaling, and normal velocity limits; Preservation of local order by variable analytic units

  1. theorem OAI.Nagata.Workers.W28.comp_coeff_eq_zero_below line 40

    Source documentation

    Low Taylor coefficients of the outer series remain zero after substitution.

    theorem comp_coeff_eq_zero_below
    (q : FormalMultilinearSeries ๐•œ F G) (p : FormalMultilinearSeries ๐•œ E F)
    (m : โ„•) (hq : โˆ€ n < m, q n = 0) :
    โˆ€ n < m, (q.comp p) n = 0 := by
โ€ฆ
  2. def OAI.Nagata.Workers.W28.HasAnalyticOrderAtLeast line 55

    Source documentation

    Genuine convergent analytic Taylor vanishing of order at least m.

    def HasAnalyticOrderAtLeast (f : E โ†’ F) (x : E) (m : โ„•) : Prop :=
โ€ฆ
  3. theorem OAI.Nagata.Workers.W28.HasAnalyticOrderAtLeast.comp line 60

    Source documentation

    Analytic substitution preserves the lower bound on Taylor order.

    theorem HasAnalyticOrderAtLeast.comp {g : F โ†’ G} {f : E โ†’ F} {x : E} {m : โ„•}
    (hg : HasAnalyticOrderAtLeast (๐•œ := ๐•œ) g (f x) m)
โ€ฆ

    Mentions: OAI.Nagata.Workers.W28.HasAnalyticOrderAtLeast

  4. theorem OAI.Nagata.Workers.W28.HasAnalyticOrderAtLeast.congr line 69

    Source documentation

    Taylor vanishing depends only on the actual local function germ.

    theorem HasAnalyticOrderAtLeast.congr {f g : E โ†’ F} {x : E} {m : โ„•}
    (hf : HasAnalyticOrderAtLeast (๐•œ := ๐•œ) f x m)
โ€ฆ

    Mentions: OAI.Nagata.Workers.W28.HasAnalyticOrderAtLeast

  5. theorem OAI.Nagata.Workers.W28.analytic_order_comp_local_chart_iff line 77

    Source documentation

    A genuine local analytic coordinate change preserves and reflects Taylor order, provided its actual inverse is analytic at the marked image.

    theorem analytic_order_comp_local_chart_iff
    (e : OpenPartialHomeomorph E F) (x : E) (hx : x โˆˆ e.source)
    (he : AnalyticAt ๐•œ e x) (hei : AnalyticAt ๐•œ e.symm (e x))
    (f : F โ†’ G) (m : โ„•) :
    HasAnalyticOrderAtLeast (๐•œ := ๐•œ) (f โˆ˜ e) x m โ†”
โ€ฆ

    Mentions: OAI.Nagata.Workers.W28.HasAnalyticOrderAtLeast

  6. theorem OAI.Nagata.Workers.W28.normal_equation_affine_velocity_limit line 108

    Source documentation

    The actual nonlinear defining equation has divided normal displacement converging to its actual derivative applied to the chosen affine velocity.

    theorem normal_equation_affine_velocity_limit
    {E : Type*} [NormedAddCommGroup E] [NormedSpace โ„‚ E]
    (G : E โ†’ โ„‚) (L : E โ†’L[โ„‚] โ„‚) (p V : E)
    (hG : HasFDerivAt G L p) (hp : G p = 0) :
    Filter.Tendsto (fun s : โ„‚ => sโปยน * G (p + s โ€ข V)) (๐“[โ‰ ] 0) (๐“ (L V)) := by
โ€ฆ
  7. theorem OAI.Nagata.VariableUnitOrder.bilinear_series_zero_second line 136

    Source documentation

    Every coefficient of a bilinear expansion at (a,0) vanishes on vectors whose second component is zero.

    theorem bilinear_series_zero_second (b : โ„‚ โ†’L[โ„‚] โ„‚ โ†’L[โ„‚] โ„‚) (a : โ„‚)
    (n : โ„•) (v : Fin n โ†’ โ„‚ ร— โ„‚) (hv : โˆ€ i, (v i).2 = 0) :
    b.fpowerSeriesBilinear (a, 0) n v = 0 := by
โ€ฆ
  8. theorem OAI.Nagata.VariableUnitOrder.product_series_coeff_zero line 147

    Source documentation

    Product composition coefficients below m vanish when the second series has no coefficients below m; this is a formal multilinear-series calculation.

    theorem product_series_coeff_zero (b : โ„‚ โ†’L[โ„‚] โ„‚ โ†’L[โ„‚] โ„‚) (a : โ„‚)
    (p q : FormalMultilinearSeries โ„‚ E โ„‚) (m : โ„•)
    (hq : โˆ€ n < m, q n = 0) :
    โˆ€ n < m, ((b.fpowerSeriesBilinear (a, 0)).comp (p.prod q)) n = 0 := by
โ€ฆ
  9. theorem OAI.Nagata.VariableUnitOrder.analytic_order_mul_left line 164

    Source documentation

    Multiplying by any actual analytic function preserves the lower Taylor-order bound.

    theorem analytic_order_mul_left {u f : E โ†’ โ„‚} {x : E} {m : โ„•}
    (hu : AnalyticAt โ„‚ u x)
    (hf : HasAnalyticOrderAtLeast (๐•œ := โ„‚) f x m) :
โ€ฆ
  10. theorem OAI.Nagata.VariableUnitOrder.analytic_order_unit_mul_iff line 187

    Source documentation

    The source's variable holomorphic-unit multiplication preserves and reflects ordinary analytic Taylor order. This includes the factor Pi(z)^(-m).

    theorem analytic_order_unit_mul_iff {u f : E โ†’ โ„‚} {x : E} (m : โ„•)
    (hu : AnalyticAt โ„‚ u x) (hu0 : u x โ‰  0) :
    HasAnalyticOrderAtLeast (๐•œ := โ„‚) (fun y => u y * f y) x m โ†”
โ€ฆ
  11. def OAI.Nagata.Workers.W28.analyticNormalScale line 209

    Source documentation

    The actual rescaling of the normal coordinate.

    def analyticNormalScale (s : โ„‚) (x : โ„‚ ร— โ„‚) : โ„‚ ร— โ„‚ := (x.1, s * x.2)
  12. theorem OAI.Nagata.Workers.W28.analyticNormalScale_analyticAt line 211
  13. theorem OAI.Nagata.Workers.W28.analyticNormalScale_inv line 217
  14. theorem OAI.Nagata.Workers.W28.analytic_order_normal_scale_iff line 223

    Source documentation

    For a nonzero specialization parameter, normal rescaling preserves and reflects the actual local convergent Taylor order.

    theorem analytic_order_normal_scale_iff
    (f : โ„‚ ร— โ„‚ โ†’ โ„‚) (s : โ„‚) (hs : s โ‰  0) (x : โ„‚ ร— โ„‚) (m : โ„•) :
    HasAnalyticOrderAtLeast (๐•œ := โ„‚) (f โˆ˜ analyticNormalScale s) x m โ†”
โ€ฆ

    Mentions: OAI.Nagata.Workers.W28.HasAnalyticOrderAtLeast, OAI.Nagata.Workers.W28.analyticNormalScale