EulerOperators.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Euler operators on formal power series

Euler operators act diagonally on coefficients, and iterated transverse derivatives shift the coefficient exponent. These formulas yield finite operators that isolate bounded exponents.

def OAI.CartierSections.eulerStep line 22
Source documentation
The Euler differential operator minus a scalar.
```
noncomputable def eulerStep (i : ι) (l : ℕ) (f : MvPowerSeries ι k) :
    MvPowerSeries ι k :=
…
```
theorem OAI.CartierSections.coeff_eulerStep line 26
def OAI.CartierSections.iterEuler line 50
theorem OAI.CartierSections.coeff_iterEuler line 54
def OAI.CartierSections.eulerFactors line 64
Source documentation
Euler factors selecting one boundary exponent among those bounded by N.
```
noncomputable def eulerFactors (B : Finset ι) (N : ℕ) (α : ι →₀ ℕ) :
    List (ι × ℕ) := by
…
```
theorem OAI.CartierSections.mem_eulerFactors line 69

theorem OAI.CartierSections.coeff_eulerFactors_self_ne_zero line 76

Source documentation

The chosen coefficient survives over a field of characteristic zero.

theorem coeff_eulerFactors_self_ne_zero (B : Finset ι) (N : ℕ)
    (α γ : ι →₀ ℕ) (hαγ : ∀ i ∈ B, γ i = α i)
    {f : MvPowerSeries ι k} (hf : MvPowerSeries.coeff γ f ≠ 0) :
    MvPowerSeries.coeff γ (iterEuler (eulerFactors B N α) f) ≠ 0 := by
…

Mentions: OAI.CartierSections.iterEuler, OAI.CartierSections.eulerFactors

theorem OAI.CartierSections.coeff_eulerFactors_eq_zero line 93

Source documentation

Every other bounded exponent in the boundary coordinates is killed.

theorem coeff_eulerFactors_eq_zero (B : Finset ι) (N : ℕ)
    (α d : ι →₀ ℕ) (hd : ∃ i ∈ B, d i ≤ N ∧ d i ≠ α i)
    (f : MvPowerSeries ι k) :
    MvPowerSeries.coeff d (iterEuler (eulerFactors B N α) f) = 0 := by
…

Mentions: OAI.CartierSections.iterEuler, OAI.CartierSections.eulerFactors

theorem OAI.CartierSections.eulerFactors_length_le line 106
Source documentation
The number of Euler factors is at most s(N+1), uniformly in the weights.
```
theorem eulerFactors_length_le (B : Finset ι) (N : ℕ) (α : ι →₀ ℕ) :
    (eulerFactors B N α).length ≤ B.card * (N+1) := by
…
```
Mentions: OAI.CartierSections.eulerFactors
def OAI.CartierSections.iterPartial line 112
def OAI.CartierSections.listExponent line 116
theorem OAI.CartierSections.listExponent_nil line 120
theorem OAI.CartierSections.listExponent_cons line 123
theorem OAI.CartierSections.coeff_iterPartial_ne_zero_iff line 132
Source documentation
Iterated transverse derivatives shift coefficients by their multidegree; the factorial coefficient is nonzero in characteristic zero.
```
theorem coeff_iterPartial_ne_zero_iff (L : List ι) (f : MvPowerSeries ι k)
    (d : ι →₀ ℕ) :
    MvPowerSeries.coeff d (iterPartial L f) ≠ 0 ↔
      MvPowerSeries.coeff (d + listExponent L) f ≠ 0 := by
…
```
Mentions: OAI.CartierSections.iterPartial, OAI.CartierSections.listExponent
theorem OAI.CartierSections.listExponent_toList line 144
theorem OAI.CartierSections.length_exponent_toList line 149