CompositeUnitMixing.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.sum_sq_unit_mixing line 12
Source documentation
The sum of unit translates has squared energy at most the number of translates squared times the original energy. This needs no primality and no positivity hypothesis on the original real-valued function.
```
theorem sum_sq_unit_mixing {q : ℕ} [NeZero q]
    {J : Type*} [Fintype J] (c : J → (ZMod q)ˣ) (w : ZMod q → ℝ) :
    (∑ x : ZMod q, (∑ j : J, w ((c j : ZMod q) * x)) ^ 2) ≤
      (Fintype.card J : ℝ) ^ 2 * ∑ x : ZMod q, w x ^ 2 := by
…
```
theorem OAI.Problem337.average_sq_unit_mixing line 41
Source documentation
Averaging arbitrary unit permutations cannot increase squared energy. In particular, adjoining independent prime choices coprime to a modulus preserves any known upper bound for the projected divisor distribution.
```
theorem average_sq_unit_mixing {q : ℕ} [NeZero q]
    {J : Type*} [Fintype J] (c : J → (ZMod q)ˣ) (w : ZMod q → ℝ) :
    (∑ x : ZMod q,
      ((∑ j : J, w ((c j : ZMod q) * x)) / (Fintype.card J : ℝ)) ^ 2) ≤
        ∑ x : ZMod q, w x ^ 2 := by
…
```

theorem OAI.Problem337.unit_mixed_fiber_count line 57

Source documentation

Multiplying an indexed sample by independent units transforms its fibers by averaging inverse unit translations. Multiplicities are retained.

theorem unit_mixed_fiber_count {q : ℕ} [NeZero q]
    {I J : Type*} [Fintype I] [Fintype J]
    (f : I → ZMod q) (c : J → (ZMod q)ˣ) (x : ZMod q) :
    (Finset.univ.filter (fun z : I × J => (c z.2 : ZMod q) * f z.1 = x)).card =
      ∑ j : J, (Finset.univ.filter
        (fun i : I => f i = ((c j)⁻¹ : (ZMod q)ˣ) * x)).card := by
…

theorem OAI.Problem337.unit_mixed_fiber_mass line 74

Source documentation

The exact normalized finite-sample mass identity used in unit mixing. The formula is valid even for an empty index type, using totalized division.

theorem unit_mixed_fiber_mass {q : ℕ} [NeZero q]
    {I J : Type*} [Fintype I] [Fintype J]
    (f : I → ZMod q) (c : J → (ZMod q)ˣ) (x : ZMod q) :
    ((Finset.univ.filter (fun z : I × J => (c z.2 : ZMod q) * f z.1 = x)).card : ℝ) /
        (Fintype.card (I × J) : ℝ) =
      (∑ j : J,
        ((Finset.univ.filter (fun i : I => f i = ((c j)⁻¹ : (ZMod q)ˣ) * x)).card : ℝ) /
          (Fintype.card I : ℝ)) / (Fintype.card J : ℝ) := by
…

theorem OAI.Problem337.indexed_energy_unit_mixing line 89

Source documentation

Adjoining an independent list of units cannot increase the normalized collision energy of a finite indexed residue sample. This is the precise nesting principle for divisor lists at moduli coprime to the added primes.

theorem indexed_energy_unit_mixing {q : ℕ} [NeZero q]
    {I J : Type*} [Fintype I] [Fintype J]
    (f : I → ZMod q) (c : J → (ZMod q)ˣ) :
    (∑ x : ZMod q,
      (((Finset.univ.filter
        (fun z : I × J => (c z.2 : ZMod q) * f z.1 = x)).card : ℝ) /
          (Fintype.card (I × J) : ℝ)) ^ 2) ≤
      ∑ x : ZMod q,
        (((Finset.univ.filter (fun i : I => f i = x)).card : ℝ) /
          (Fintype.card I : ℝ)) ^ 2 := by
…