ExponentialProductChart.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Local product charts from the finite Dynkin identity

Products of exponentials in a basis have a locally surjective logarithm map. The proof gets smoothness from the finite Dynkin polynomial and its derivative from the exact one-coordinate restrictions. No smooth-logarithm or local product assertion is a separate input.

theorem OAI.PolycyclicRecognition.list_prod_ofFn_eq_single line 26
Source documentation
An ordered product with just one nonidentity factor equals that factor, without a commutativity assumption.
```
theorem list_prod_ofFn_eq_single {G : Type*} [Monoid G] {n : ℕ}
    (f : Fin n → G) (i : Fin n) (hf : ∀ j, j ≠ i → f j = 1) :
    (List.ofFn f).prod = f i := by
…
```

def OAI.PolycyclicRecognition.basisExponentialProduct line 46

Source documentation

The ordered basis-exponential endpoint map.

def basisExponentialProduct {L G : Type*} [AddCommGroup L] [Module ℝ L]
    [Monoid G] {n : ℕ} (Exp : L → G) (b : Basis (Fin n) ℝ L) (t : Fin n → ℝ) : G :=
…

def OAI.PolycyclicRecognition.basisProductLog line 61
Source documentation
Its logarithm in a global exponential bijection.
```
def basisProductLog (hExp : Function.Bijective Exp) (t : Fin n → ℝ) : L :=
…
```
theorem OAI.PolycyclicRecognition.basisProductLog_zero line 67
theorem OAI.PolycyclicRecognition.basisProductLog_single line 74
theorem OAI.PolycyclicRecognition.contDiff_basisProductLog line 89
Source documentation
The exact polynomial identity supplies all differentiability of the logarithmic endpoint map.
```
theorem contDiff_basisProductLog {c : ℕ} (coeff : DynkinCoefficients c n)
    (hprod : ∀ X : Fin n → L, (List.ofFn (fun i => Exp (X i))).prod =
      Exp (finiteDynkinPolynomial coeff X)) :
    ContDiff ℝ ∞ (basisProductLog Exp b hExp) := by
…
```
Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.finiteDynkinPolynomial, OAI.PolycyclicRecognition.basisProductLog
theorem OAI.PolycyclicRecognition.fderiv_basisProductLog_zero line 105
Source documentation
The differential of the logarithmic endpoint map at the origin is the basis synthesis map, proved from its coordinate-axis restrictions.
```
theorem fderiv_basisProductLog_zero
    (hd : DifferentiableAt ℝ (basisProductLog Exp b hExp) 0) :
    fderiv ℝ (basisProductLog Exp b hExp) 0 = b.equivFun.symm.toContinuousLinearEquiv := by
…
```
Mentions: OAI.PolycyclicRecognition.basisProductLog
theorem OAI.PolycyclicRecognition.basisProductLog_map_nhds line 130
Source documentation
The basis exponential map covers a logarithmic neighborhood using parameters from any prescribed neighborhood of zero.
```
theorem basisProductLog_map_nhds {c : ℕ} (coeff : DynkinCoefficients c n)
    (hprod : ∀ X : Fin n → L, (List.ofFn (fun i => Exp (X i))).prod =
      Exp (finiteDynkinPolynomial coeff X)) :
    map (basisProductLog Exp b hExp) (𝓝 0) = 𝓝 (0 : L) := by
…
```
Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.finiteDynkinPolynomial, OAI.PolycyclicRecognition.basisProductLog

theorem OAI.PolycyclicRecognition.exists_ball_subset_basisProductLog_image line 145

Source documentation

A fixed parameter ball suffices for a nonzero logarithmic ball.

theorem exists_ball_subset_basisProductLog_image {c : ℕ} (coeff : DynkinCoefficients c n)
    (hprod : ∀ X : Fin n → L, (List.ofFn (fun i => Exp (X i))).prod =
      Exp (finiteDynkinPolynomial coeff X)) :
    ∃ ε : ℝ, 0 < ε ∧ Metric.ball (0 : L) ε ⊆
      basisProductLog Exp b hExp '' Metric.ball (0 : Fin n → ℝ) 1 := by
…

Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.finiteDynkinPolynomial, OAI.PolycyclicRecognition.basisProductLog