AnalyticJets.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Analytic scalar families, moving jets, and cofinite jet limits

theorem OAI.Nagata.Workers.W17.continuous_value_zero_of_cofinite line 30
Source documentation
A continuous quantity vanishing outside a finite parameter set vanishes at the limiting parameter, including when the parameter lies in that set.
```
theorem continuous_value_zero_of_cofinite
    (f : 𝕜 → V) (x : 𝕜) (exceptional : Finset 𝕜)
    (hf : ContinuousAt f x) (hzero : ∀ s, s ∉ exceptional → f s = 0) :
    f x = 0 := by
…
```

theorem OAI.Nagata.Workers.W17.continuous_value_zero_of_eventually_cofinite line 41

Source documentation

Local version: only a neighborhood of the limiting parameter is needed.

theorem continuous_value_zero_of_eventually_cofinite
    (f : 𝕜 → V) (x : 𝕜) (exceptional : Finset 𝕜)
    (hf : ContinuousAt f x)
    (hzero : ∀ᶠ s in 𝓝 x, s ∉ exceptional → f s = 0) : f x = 0 := by
…

theorem OAI.Nagata.Workers.W17.cofinite_moving_derivative_jets line 60

Source documentation

Genuine low-order derivative jets survive a cofinite parameter limit. Continuity is explicitly required and is not hidden in a substitute object.

theorem cofinite_moving_derivative_jets
    (family : 𝕜 → E → F) (center : 𝕜 → E) (x : 𝕜)
    (exceptional : Finset 𝕜) (m : Nat)
    (hcontinuous : ∀ n < m,
      ContinuousAt (fun s => iteratedFDeriv 𝕜 n (family s) (center s)) x)
    (hjets : ∀ s, s ∉ exceptional → ∀ n < m,
      iteratedFDeriv 𝕜 n (family s) (center s) = 0) :
    ∀ n < m, iteratedFDeriv 𝕜 n (family x) (center x) = 0 := by
…

theorem OAI.Nagata.Workers.W17.local_cofinite_moving_derivative_jets line 75

Source documentation

The source application: the holomorphic family and its jet identities need only hold near the limiting parameter outside finitely many values.

theorem local_cofinite_moving_derivative_jets
    (family : 𝕜 → E → F) (center : 𝕜 → E) (x : 𝕜)
    (exceptional : Finset 𝕜) (m : Nat)
    (hcontinuous : ∀ n < m,
      ContinuousAt (fun s => iteratedFDeriv 𝕜 n (family s) (center s)) x)
    (hjets : ∀ᶠ s in 𝓝 x, s ∉ exceptional → ∀ n < m,
      iteratedFDeriv 𝕜 n (family s) (center s) = 0) :
    ∀ n < m, iteratedFDeriv 𝕜 n (family x) (center x) = 0 := by
…

theorem OAI.Nagata.Workers.W17.powerSeries_diagonal_zero_of_iteratedFDeriv_zero line 107

Source documentation

The diagonal of a Taylor coefficient vanishes when its derivative does.

theorem powerSeries_diagonal_zero_of_iteratedFDeriv_zero
    {f : E → F} {x : E} {p : FormalMultilinearSeries 𝕜 E F} {n : ℕ}
    (hp : HasFPowerSeriesAt f p x) (hn : iteratedFDeriv 𝕜 n f x = 0) (v : E) :
    p n (fun _ => v) = 0 := by
…

theorem OAI.Nagata.Workers.W17.analytic_order_of_iteratedFDeriv_zero line 121

Source documentation

Actual analytic derivatives detect the existential convergent Taylor order.

theorem analytic_order_of_iteratedFDeriv_zero
    {f : E → F} {x : E} (hf : AnalyticAt 𝕜 f x) (m : ℕ)
    (hz : ∀ n < m, iteratedFDeriv 𝕜 n f x = 0) :
    HasAnalyticOrderAtLeast (𝕜 := 𝕜) f x m := by
…

theorem OAI.Nagata.Workers.W17.analytic_order_const_smul line 169
Source documentation
Multiplication by a constant preserves lower Taylor order.
```
theorem analytic_order_const_smul {f : E → F} {x : E} {m : Nat}
    (hf : HasAnalyticOrderAtLeast (𝕜 := 𝕜) f x m) (c : 𝕜) :
…
```

theorem OAI.Nagata.Workers.W17.analytic_order_const_smul_iff line 178

Source documentation

A nonzero scalar preserves and reflects analytic Taylor order.

theorem analytic_order_const_smul_iff (f : E → F) (x : E) (m : Nat)
    (c : 𝕜) (hc : c ≠ 0) :
    HasAnalyticOrderAtLeast (𝕜 := 𝕜) (c • f) x m ↔
…

theorem OAI.Nagata.Workers.W17.analytic_order_const_mul_iff line 190

Source documentation

Scalar multiplication of a scalar-valued section in a local frame.

theorem analytic_order_const_mul_iff (f : E → 𝕜) (x : E) (m : Nat)
    (c : 𝕜) (hc : c ≠ 0) :
    HasAnalyticOrderAtLeast (𝕜 := 𝕜) (fun y => c * f y) x m ↔
…

theorem OAI.Nagata.Workers.W17.contDiffAt_parameter_iteratedFDeriv line 222

Source documentation

Fiber-variable iterated derivatives of a jointly smooth family are jointly smooth, proved by parameterized differentiation.

theorem contDiffAt_parameter_iteratedFDeriv
    (family : P → E → F) (p : P × E)
    (hf : ContDiffAt 𝕜 ∞ (Function.uncurry family) p) (n : Nat) :
    ContDiffAt 𝕜 ∞ (fun q : P × E => iteratedFDeriv 𝕜 n (family q.1) q.2) p := by
…

theorem OAI.Nagata.Workers.W17.analytic_moving_derivative_continuousAt line 253

Source documentation

Joint analyticity supplies continuity of all ordinary fiber jets along any continuous moving center.

theorem analytic_moving_derivative_continuousAt [CompleteSpace F]
    (family : P → E → F) (center : P → E) (s₀ : P)
    (hf : AnalyticAt 𝕜 (Function.uncurry family) (s₀, center s₀))
    (hc : ContinuousAt center s₀) (n : Nat) :
    ContinuousAt (fun s => iteratedFDeriv 𝕜 n (family s) (center s)) s₀ := by
…

theorem OAI.Nagata.Workers.W17.analytic_local_cofinite_moving_derivative_jets line 267

Source documentation

Thus actual cofinite jet vanishing specializes in a jointly analytic family without any separately assumed derivative-continuity hypothesis.

theorem analytic_local_cofinite_moving_derivative_jets [CompleteSpace F]
    (family : 𝕜 → E → F) (center : 𝕜 → E) (s₀ : 𝕜)
    (exceptional : Finset 𝕜) (m : Nat)
    (hf : AnalyticAt 𝕜 (Function.uncurry family) (s₀, center s₀))
    (hc : ContinuousAt center s₀)
    (hjets : ∀ᶠ s in nhds s₀, s ∉ exceptional → ∀ n < m,
      iteratedFDeriv 𝕜 n (family s) (center s) = 0) :
    ∀ n < m, iteratedFDeriv 𝕜 n (family s₀) (center s₀) = 0 := by
…