Convolution.lean`

61 declarations, 0 contain sorry, 0 declared as axioms

Coordinate masks and permutations on the actual complex square-summable space. These implement the Hilbert-space operations used in lem:length-one-convolution.

abbrev OAI.Generator.SquareSpace line 19
theorem OAI.Generator.squareSpace_norm_sq line 23
def OAI.Generator.coordinateMask line 27
theorem OAI.Generator.coordinateMask_apply line 31
theorem OAI.Generator.coordinateMask_norm_le line 34
theorem OAI.Generator.coordinateMask_add_compl line 40
def OAI.Generator.coordinatePermute line 46
theorem OAI.Generator.coordinatePermute_apply line 49
theorem OAI.Generator.coordinatePermute_norm line 52
def OAI.Generator.coordinatePermuteCLM line 60
Source documentation
Reindexing by a permutation, as a bounded complex linear operator.
```
def coordinatePermuteCLM (e : X ≃ X) : SquareSpace X →L[ℂ] SquareSpace X :=
…
```
Mentions: OAI.Generator.SquareSpace
theorem OAI.Generator.coordinatePermuteCLM_apply line 67
theorem OAI.Generator.squareSpace_inner_zero line 71
Source documentation
Disjoint coordinate support implies genuine Hilbert orthogonality.
```
theorem squareSpace_inner_zero {f g : SquareSpace X}
    (h : ∀ x, f x = 0 ∨ g x = 0) : inner ℂ f g = 0 := by
…
```
Mentions: OAI.Generator.SquareSpace

theorem OAI.Generator.squareSpace_sum_norm_sq line 80

Source documentation

Pythagoras for a finite family with disjoint supports.

theorem squareSpace_sum_norm_sq (s : Finset I) (f : I → SquareSpace X)
    (h : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → ∀ x, f i x = 0 ∨ f j x = 0) :
    ‖∑ i ∈ s, f i‖ ^ 2 = ∑ i ∈ s, ‖f i‖ ^ 2 := by
…

Mentions: OAI.Generator.SquareSpace

theorem OAI.Generator.coordinateMask_sum_sq_le line 97
Source documentation
The projections onto finitely many disjoint coordinate sets have total squared mass at most that of the original vector.
```
theorem coordinateMask_sum_sq_le (s : Finset I) (U : I → Set X)
    (hU : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (U i) (U j))
    (f : SquareSpace X) :
    ∑ i ∈ s, ‖coordinateMask (U i) f‖ ^ 2 ≤ ‖f‖ ^ 2 := by
…
```
Mentions: OAI.Generator.SquareSpace, OAI.Generator.coordinateMask
abbrev OAI.Generator.FreeConvolution.Letter line 138
def OAI.Generator.FreeConvolution.inverseLetter line 140
def OAI.Generator.FreeConvolution.letter line 141
def OAI.Generator.FreeConvolution.begins line 142
theorem OAI.Generator.FreeConvolution.inverseLetter_inverse line 144
theorem OAI.Generator.FreeConvolution.inverseLetter_injective line 147
theorem OAI.Generator.FreeConvolution.letter_toWord line 150
theorem OAI.Generator.FreeConvolution.letter_inverse line 153
theorem OAI.Generator.FreeConvolution.letter_true line 156
theorem OAI.Generator.FreeConvolution.letter_false line 158
theorem OAI.Generator.FreeConvolution.letter_injective line 161
theorem OAI.Generator.FreeConvolution.begins_letter_mul line 167
Source documentation
A noncancelling left multiplication creates its signed letter as the head.
```
theorem begins_letter_mul (a : Letter A) (w : FreeGroup A)
    (h : ¬ begins (inverseLetter a) w) : begins a (letter a * w) := by
…
```
Mentions: OAI.Generator.FreeConvolution.Letter, OAI.Generator.FreeConvolution.begins, OAI.Generator.FreeConvolution.inverseLetter, OAI.Generator.FreeConvolution.letter
def OAI.Generator.FreeConvolution.leftRegular line 185
Source documentation
The actual left regular translation λ(g)η(x)=η(g⁻¹x).
```
def leftRegular (g : FreeGroup A) : SquareSpace (FreeGroup A) →L[ℂ] SquareSpace (FreeGroup A) :=
…
```
Mentions: OAI.Generator.SquareSpace
theorem OAI.Generator.FreeConvolution.leftRegular_apply line 188
theorem OAI.Generator.FreeConvolution.leftRegular_norm line 191
def OAI.Generator.FreeConvolution.creation line 194
def OAI.Generator.FreeConvolution.cancellation line 197
theorem OAI.Generator.FreeConvolution.creation_add_cancellation line 200
theorem OAI.Generator.FreeConvolution.creation_support line 209
theorem OAI.Generator.FreeConvolution.begins_disjoint line 217
theorem OAI.Generator.FreeConvolution.creation_norm_le line 223
theorem OAI.Generator.FreeConvolution.creation_sum_bound line 228
theorem OAI.Generator.FreeConvolution.cancellation_sum_bound line 253
theorem OAI.Generator.FreeConvolution.length_one_convolution_vector_bound line 270
Source documentation
The manuscript's length-one bound on every vector of ℓ²(FreeGroup A).
```
theorem length_one_convolution_vector_bound (s : Finset (Letter A)) (b : Letter A → ℂ)
    (f : SquareSpace (FreeGroup A)) :
    ‖(∑ a ∈ s, b a • leftRegular (letter a)) f‖ ≤
      (2 * Real.sqrt (∑ a ∈ s, ‖b a‖ ^ 2)) * ‖f‖ := by
…
```
Mentions: OAI.Generator.FreeConvolution.Letter, OAI.Generator.SquareSpace, OAI.Generator.FreeConvolution.leftRegular, OAI.Generator.FreeConvolution.letter
theorem OAI.Generator.FreeConvolution.length_one_convolution_operator_bound line 285
Source documentation
The length-one convolution estimate for the operator norm of the left regular action.
```
theorem length_one_convolution_operator_bound (s : Finset (Letter A)) (b : Letter A → ℂ) :
    ‖∑ a ∈ s, b a • leftRegular (letter a)‖ ≤
      2 * Real.sqrt (∑ a ∈ s, ‖b a‖ ^ 2) := by
…
```
Mentions: OAI.Generator.FreeConvolution.Letter, OAI.Generator.FreeConvolution.leftRegular, OAI.Generator.FreeConvolution.letter
def OAI.Generator.FreeConvolution.leftRegularHom line 304
def OAI.Generator.FreeConvolution.regular line 309
def OAI.Generator.FreeConvolution.realRegular line 312
def OAI.Generator.FreeConvolution.delta line 315
theorem OAI.Generator.FreeConvolution.delta_apply line 317
theorem OAI.Generator.FreeConvolution.delta_norm line 320
theorem OAI.Generator.FreeConvolution.leftRegular_delta_apply line 323
theorem OAI.Generator.FreeConvolution.regular_delta_apply line 328
Source documentation
Applying the actual convolution operator to δ₁ recovers every coefficient.
```
theorem regular_delta_apply (f : MonoidAlgebra ℂ (FreeGroup A)) (x : FreeGroup A) :
    regular f delta x = f.coeff x := by
…
```
Mentions: OAI.Generator.FreeConvolution.regular, OAI.Generator.FreeConvolution.delta
theorem OAI.Generator.FreeConvolution.realRegular_delta_apply line 335
theorem OAI.Generator.FreeConvolution.regular_single_delta line 344
theorem OAI.Generator.FreeConvolution.regular_delta_orthonormal line 350
theorem OAI.Generator.FreeConvolution.regular_coefficient_isometry line 368
Source documentation
Exact finite coefficient L² isometry in the regular representation.
```
theorem regular_coefficient_isometry (f : MonoidAlgebra ℂ (FreeGroup A)) :
    ‖regular f delta‖ ^ 2 = ∑ x ∈ f.coeff.support, ‖f.coeff x‖ ^ 2 := by
…
```
Mentions: OAI.Generator.FreeConvolution.regular, OAI.Generator.FreeConvolution.delta
theorem OAI.Generator.FreeConvolution.regular_delta_norm_le line 378
Source documentation
Coefficient domination implies the ℓ² inequality; no comparison between operator norms in distinct representations is used.
```
theorem regular_delta_norm_le {f : MonoidAlgebra ℂ (FreeGroup A)}
    {a : MonoidAlgebra ℝ (FreeGroup A)} (h : ∀ x, ‖f.coeff x‖ ≤ a.coeff x) :
    ‖regular f delta‖ ≤ ‖realRegular a delta‖ := by
…
```
Mentions: OAI.Generator.FreeConvolution.regular, OAI.Generator.FreeConvolution.delta, OAI.Generator.FreeConvolution.realRegular
theorem OAI.Generator.FreeConvolution.realRegular_pow_delta_norm_le line 387
Source documentation
Actual coefficient-vector power estimate.
```
theorem realRegular_pow_delta_norm_le (a : MonoidAlgebra ℝ (FreeGroup A)) (d : ℕ) :
    ‖realRegular (a ^ d) delta‖ ≤ ‖realRegular a‖ ^ d := by
…
```
Mentions: OAI.Generator.FreeConvolution.realRegular, OAI.Generator.FreeConvolution.delta

theorem OAI.Generator.groupRing_linear_combination line 407

Source documentation

Linear images of a group-ring sum are its literal finite coefficient combination.

theorem groupRing_linear_combination (Ψ : MonoidAlgebra ℂ G →ₗ[ℂ] E)
    (f : MonoidAlgebra ℂ G) :
    Ψ f = ∑ g ∈ f.coeff.support, f.coeff g • Ψ (MonoidAlgebra.single g 1) := by
…

theorem OAI.Generator.groupRing_coefficient_isometry line 419

Source documentation

The source's coefficient isometry from actual orthonormal word images.

theorem groupRing_coefficient_isometry (Ψ : MonoidAlgebra ℂ G →ₗ[ℂ] E)
    (hΨ : Orthonormal ℂ (fun g => Ψ (MonoidAlgebra.single g 1)))
    (f : MonoidAlgebra ℂ G) :
    ‖Ψ f‖ ^ 2 = ∑ g ∈ f.coeff.support, ‖f.coeff g‖ ^ 2 := by
…

theorem OAI.Generator.groupRing_norm_eq_of_orthonormal line 431

Source documentation

Two orthonormal realizations have exactly the same coefficient norm.

theorem groupRing_norm_eq_of_orthonormal {E' : Type*} [NormedAddCommGroup E']
    [InnerProductSpace ℂ E'] (Ψ : MonoidAlgebra ℂ G →ₗ[ℂ] E)
    (Θ : MonoidAlgebra ℂ G →ₗ[ℂ] E')
    (hΨ : Orthonormal ℂ (fun g => Ψ (MonoidAlgebra.single g 1)))
    (hΘ : Orthonormal ℂ (fun g => Θ (MonoidAlgebra.single g 1)))
    (f : MonoidAlgebra ℂ G) : ‖Ψ f‖ = ‖Θ f‖ := by
…

theorem OAI.Generator.groupRing_norm_eq_regular line 442

Source documentation

For orthonormal word images, the finite coefficient norm agrees with the regular representation norm.

theorem groupRing_norm_eq_regular {A : Type*}
    (Ψ : MonoidAlgebra ℂ (FreeGroup A) →ₗ[ℂ] E)
    (hΨ : Orthonormal ℂ (fun g => Ψ (MonoidAlgebra.single g 1)))
    (f : MonoidAlgebra ℂ (FreeGroup A)) :
    ‖Ψ f‖ = ‖FreeConvolution.regular f FreeConvolution.delta‖ := by
…

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

def OAI.Generator.prefixLetterSupport line 457
def OAI.Generator.prefixWeight line 460
theorem OAI.Generator.prefixWeight_square_sum_le line 464
Source documentation
The exact collected multiplicities imply the required square-coefficient budget.
```
theorem prefixWeight_square_sum_le (n : ℕ) (hn : 0 < n) (α : ℝ) :
    ∑ a ∈ prefixLetterSupport n, ‖(prefixWeight n α a : ℂ)‖ ^ 2 ≤ α ^ 2 := by
…
```
Mentions: OAI.Generator.prefixLetterSupport, OAI.Generator.prefixWeight
theorem OAI.Generator.prefix_convolution_operator_bound line 490
Source documentation
The manuscript's actual coefficient family has convolution norm at most 2α.
```
theorem prefix_convolution_operator_bound (n : ℕ) (hn : 0 < n)
    (α : ℝ) (hα : 0 ≤ α) :
    ‖∑ a ∈ prefixLetterSupport n, (prefixWeight n α a : ℂ) • leftRegular (letter a)‖ ≤
      2 * α := by
…
```
Mentions: OAI.Generator.prefixLetterSupport, OAI.Generator.prefixWeight