LongWords.lean`

39 declarations, 0 contain sorry, 0 declared as axioms

Factorial coefficient majorization in every homogeneous degree.

theorem OAI.Generator.normCoefficients_zero line 19
theorem OAI.Generator.normCoefficients_one line 22
theorem OAI.Generator.normCoefficients_single line 30
theorem OAI.Generator.normCoefficients_sub_le line 37
theorem OAI.Generator.normCoefficients_sum_le line 42
theorem OAI.Generator.normCoefficients_pow_le line 51
theorem OAI.Generator.normCoefficients_real_smul line 61

theorem OAI.Generator.exponentialDegree_le_orderedWords line 67

Source documentation

Original-degree factorial terms are bounded by nondecreasing row words.

theorem exponentialDegree_le_orderedWords
    (rows : List (MonoidAlgebra ℂ G × MonoidAlgebra ℝ G))
    (h : ∀ row ∈ rows, 0 ≤ row.2 ∧ normCoefficients row.1 ≤ row.2) (d : ℕ) :
    normCoefficients (exponentialDegree (rows.map Prod.fst) d) ≤
      orderedWords (rows.map Prod.snd) d := by
…

Mentions: OAI.Generator.normCoefficients, OAI.Generator.exponentialDegree, OAI.Generator.orderedWords

theorem OAI.Generator.exponentialDegree_coefficient_majorization line 105

Source documentation

The source's full coefficient inequality, for arbitrary monoids and all d. The sum on the right is the actual collected convolution power.

theorem exponentialDegree_coefficient_majorization
    (rows : List (MonoidAlgebra ℂ G × MonoidAlgebra ℝ G))
    (h : ∀ row ∈ rows, 0 ≤ row.2 ∧ normCoefficients row.1 ≤ row.2) (d : ℕ) :
    normCoefficients (exponentialDegree (rows.map Prod.fst) d) ≤
      (rows.map Prod.snd).sum ^ d := by
…

Mentions: OAI.Generator.normCoefficients, OAI.Generator.exponentialDegree

theorem OAI.Generator.free_exponentialDegree_bound line 129

Source documentation

All original-degree bounds follow from coefficient majorization and the norm of the positive total convolution operator.

theorem free_exponentialDegree_bound
    (rows : List (MonoidAlgebra ℂ (FreeGroup A) × MonoidAlgebra ℝ (FreeGroup A)))
    (h : ∀ row ∈ rows, 0 ≤ row.2 ∧ normCoefficients row.1 ≤ row.2) (d : ℕ) :
    ‖regular (exponentialDegree (rows.map Prod.fst) d) delta‖ ≤
      ‖realRegular (rows.map Prod.snd).sum‖ ^ d := by
…

Mentions: OAI.Generator.normCoefficients, OAI.Generator.exponentialDegree

theorem OAI.Generator.free_exponential_product_remainder line 139

Source documentation

Actual nonlinear remainder. The positive total's norm bound is the only analytic bound required; no degree-bound or series-sum hypothesis is assumed.

theorem free_exponential_product_remainder
    (rows : List (MonoidAlgebra ℂ (FreeGroup A) × MonoidAlgebra ℝ (FreeGroup A)))
    (h : ∀ row ∈ rows, 0 ≤ row.2 ∧ normCoefficients row.1 ≤ row.2)
    {α : ℝ} (hα : 0 < α) (hhalf : α < 1 / 2)
    (hbound : ‖realRegular (rows.map Prod.snd).sum‖ ≤ 2 * α) :
    ‖((rows.map (fun r => NormedSpace.exp (regular r.1))).prod - 1 -
      (rows.map (fun r => regular r.1)).sum) delta‖ ≤ 4 * α ^ 2 / (1 - 2 * α) := by
…

Mentions: OAI.Generator.normCoefficients

def OAI.Generator.positiveLetterPair line 176
def OAI.Generator.negativeLetterPair line 179
def OAI.Generator.perturbationRow line 182
def OAI.Generator.perturbationRows line 186
theorem OAI.Generator.positiveLetterPair_nonnegative line 189
theorem OAI.Generator.negativeLetterPair_dominated line 195
theorem OAI.Generator.perturbationRows_dominated line 202
Source documentation
Positivity and domination are proved for the source rows, not assumed.
```
theorem perturbationRows_dominated (n : ℕ) (α : ℝ) (hα : 0 ≤ α) :
    ∀ row ∈ perturbationRows n α, 0 ≤ row.2 ∧ normCoefficients row.1 ≤ row.2 := by
…
```
Mentions: OAI.Generator.perturbationRows, OAI.Generator.normCoefficients

theorem OAI.Generator.pairRatio_sum_multiplicity line 223

Source documentation

Exact regrouping of the ordered-pair sum using the proved fiber counts.

theorem pairRatio_sum_multiplicity {R : Type*} [AddCommMonoid R]
    (n : ℕ) (hn : 0 < n) (f : G → R) :
    (∑ k : Fin n, ∑ j : Fin n, f (pairRatio (k, j))) =
      ∑ p ∈ ratioLabels n, multiplicity n p • f p := by
…

Mentions: OAI.Generator.pairRatio, OAI.Generator.ratioLabels, OAI.Generator.multiplicity

theorem OAI.Generator.perturbationRows_positive_total line 236
Source documentation
The sum of the source's positive rows is exactly its collected coefficient family, including the n copies of the identity prefix ratio.
```
theorem perturbationRows_positive_total (n : ℕ) (hn : 0 < n) (α : ℝ) :
    (perturbationRows n α |>.map Prod.snd).sum =
      (α / (2 * n)) • ∑ p ∈ ratioLabels n, multiplicity n p • positiveLetterPair p := by
…
```
Mentions: OAI.Generator.perturbationRows, OAI.Generator.ratioLabels, OAI.Generator.multiplicity, OAI.Generator.positiveLetterPair
theorem OAI.Generator.perturbationRows_total_operator line 243
Source documentation
Identification of λ(A) with the signed-letter operator already bounded.
```
theorem perturbationRows_total_operator (n : ℕ) (hn : 0 < n) (α : ℝ) :
    realRegular (perturbationRows n α |>.map Prod.snd).sum =
      ∑ a ∈ prefixLetterSupport n, (prefixWeight n α a : ℂ) • leftRegular (letter a) := by
…
```
Mentions: OAI.Generator.perturbationRows, OAI.Generator.prefixLetterSupport, OAI.Generator.prefixWeight

theorem OAI.Generator.perturbationRows_degree_bound line 258

Source documentation

Uniform all-degree bound for the manuscript's literal formal rows.

theorem perturbationRows_degree_bound (n : ℕ) (hn : 0 < n)
    (α : ℝ) (hα : 0 ≤ α) (d : ℕ) :
    ‖regular (exponentialDegree (perturbationRows n α |>.map Prod.fst) d) delta‖ ≤
      (2 * α) ^ d := by
…

Mentions: OAI.Generator.exponentialDegree, OAI.Generator.perturbationRows

theorem OAI.Generator.perturbationRows_remainder line 269

Source documentation

The source's nonlinear estimate on the actual regular representation, with its exact rows and constants, for every positive word length.

theorem perturbationRows_remainder (n : ℕ) (hn : 0 < n)
    (α : ℝ) (hα : 0 < α) (hhalf : α < 1 / 2) :
    ‖((perturbationRows n α |>.map (fun r => NormedSpace.exp (regular r.1))).prod - 1 -
      (perturbationRows n α |>.map (fun r => regular r.1)).sum) delta‖ ≤
        4 * α ^ 2 / (1 - 2 * α) := by
…

Mentions: OAI.Generator.perturbationRows

theorem OAI.Generator.perturbationRows_remainder_transfer line 291

Source documentation

The literal source remainder in any continuous Hilbert realization whose reduced-word images are orthonormal.

theorem perturbationRows_remainder_transfer
    (Φ : MonoidAlgebra ℂ F →ₐ[ℂ] B) (ι : B →L[ℂ] E)
    (horth : Orthonormal ℂ (fun g => ι (Φ (MonoidAlgebra.single g 1))))
    (n : ℕ) (hn : 0 < n) (α : ℝ) (hα : 0 < α) (hhalf : α < 1 / 2) :
    ‖ι ((perturbationRows n α |>.map (fun r => NormedSpace.exp (Φ r.1))).prod -
      1 - (perturbationRows n α |>.map (fun r => Φ r.1)).sum)‖ ≤
        4 * α ^ 2 / (1 - 2 * α) := by
…

Mentions: OAI.Generator.perturbationRows

def OAI.Generator.PrefixLabel line 334
Source documentation
The manuscript's finite set S, including the identity prefix ratio as a label.
```
def PrefixLabel (n : ℕ) := {p : G // p ∈ ratioLabels n}
```
Mentions: OAI.Generator.ratioLabels
def OAI.Generator.pairLabel line 336
def OAI.Generator.prefixWordEmbedding line 341
theorem OAI.Generator.prefixWordEmbedding_injective line 344
def OAI.Generator.prefixRingEmbedding line 347
theorem OAI.Generator.prefixRingEmbedding_single line 350
def OAI.Generator.finitePerturbationRow line 356
Source documentation
Literal B_k in the free group on the finite label set S.
```
def finitePerturbationRow {n : ℕ} (α : ℝ) (k : Fin n) :
    MonoidAlgebra ℂ (FreeGroup (PrefixLabel n)) :=
…
```
Mentions: OAI.Generator.PrefixLabel
def OAI.Generator.finitePerturbationRows line 362
theorem OAI.Generator.finitePerturbationRow_embed line 365
theorem OAI.Generator.finitePerturbationRows_embed line 374
def OAI.Generator.embeddedCoefficientMap line 379
theorem OAI.Generator.embeddedCoefficientMap_orthonormal line 384
theorem OAI.Generator.finitePerturbationRows_degree_bound line 390
Source documentation
All-degree estimate on the exact finite formal group F_S.
```
theorem finitePerturbationRows_degree_bound (n : ℕ) (hn : 0 < n)
    (α : ℝ) (hα : 0 ≤ α) (d : ℕ) :
    ‖embeddedCoefficientMap n (exponentialDegree (finitePerturbationRows n α) d)‖ ≤
      (2 * α) ^ d := by
…
```
Mentions: OAI.Generator.embeddedCoefficientMap, OAI.Generator.exponentialDegree, OAI.Generator.finitePerturbationRows

theorem OAI.Generator.finite_prefix_remainder_transfer line 411

Source documentation

Remainder bounds in a continuous Hilbert realization of the finite free group with orthonormal word images.

theorem finite_prefix_remainder_transfer (n : ℕ) (hn : 0 < n)
    (Φ : MonoidAlgebra ℂ (FreeGroup (PrefixLabel n)) →ₐ[ℂ] B) (ι : B →L[ℂ] E)
    (horth : Orthonormal ℂ (fun g => ι (Φ (MonoidAlgebra.single g 1))))
    (α : ℝ) (hα : 0 < α) (hhalf : α < 1 / 2) :
    ‖ι ((finitePerturbationRows n α |>.map (fun r => NormedSpace.exp (Φ r))).prod -
      1 - (finitePerturbationRows n α |>.map Φ).sum)‖ ≤
        4 * α ^ 2 / (1 - 2 * α) := by
…

Mentions: OAI.Generator.PrefixLabel, OAI.Generator.finitePerturbationRows

theorem OAI.Generator.finite_prefix_regular_remainder line 440

Source documentation

The unconditional finite-free-group remainder, on the actual left regular representation of exactly F_S and for every positive word length.

theorem finite_prefix_regular_remainder (n : ℕ) (hn : 0 < n)
    (α : ℝ) (hα : 0 < α) (hhalf : α < 1 / 2) :
    ‖((finitePerturbationRows n α |>.map (fun r => NormedSpace.exp (FreeConvolution.regular r))).prod -
      1 - (finitePerturbationRows n α |>.map FreeConvolution.regular).sum)
        FreeConvolution.delta‖ ≤ 4 * α ^ 2 / (1 - 2 * α) := by
…

Mentions: OAI.Generator.finitePerturbationRows, OAI.Generator.FreeConvolution.regular, OAI.Generator.FreeConvolution.delta