DivisorEnergyNesting.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.coprimeDivisorProductEquiv line 11
Source documentation
Multiplication bijects the divisor lists of two coprime integers with the divisor list of their product.
```
def coprimeDivisorProductEquiv {P R : ℕ} (hPR : P.Coprime R) :
    (↥P.divisors × ↥R.divisors) ≃ ↥(P * R).divisors := by
…
```
theorem OAI.Problem337.coprimeDivisorProductEquiv_val line 36

theorem OAI.Problem337.fiber_mass_equiv line 41

Source documentation

Reindexing an indexed sample preserves each normalized fiber mass.

theorem fiber_mass_equiv {I J X : Type*} [Fintype I] [Fintype J]
    [DecidableEq X] (e : I ≃ J) (f : J → X) (x : X) :
    ((Finset.univ.filter (fun i : I => f (e i) = x)).card : ℝ) /
        (Fintype.card I : ℝ) =
      ((Finset.univ.filter (fun j : J => f j = x)).card : ℝ) /
        (Fintype.card J : ℝ) := by
…

def OAI.Problem337.divisorResidueEnergy line 55
Source documentation
The normalized residue-fiber energy of the complete positive divisor list.
```
def divisorResidueEnergy (P q : ℕ) [NeZero q] : ℝ :=
…
```
theorem OAI.Problem337.divisorResidueEnergy_mul_le line 62
Source documentation
Appending coprime factors which are units modulo q cannot increase the normalized collision energy of the actual complete divisor list.
```
theorem divisorResidueEnergy_mul_le {P R q : ℕ} [NeZero q]
    (hPR : P.Coprime R) (hRq : R.Coprime q) :
    divisorResidueEnergy (P * R) q ≤ divisorResidueEnergy P q := by
…
```
Mentions: OAI.Problem337.divisorResidueEnergy
theorem OAI.Problem337.divisorResidueEnergy_le_of_dvd_squarefree line 85
Source documentation
The form used for nested prime-prefix products: at a modulus coprime to the larger squarefree supply, enlarging the supply decreases energy.
```
theorem divisorResidueEnergy_le_of_dvd_squarefree {P Q q : ℕ} [NeZero q]
    (hPQ : P ∣ Q) (hQ : Squarefree Q) (hQq : Q.Coprime q) :
    divisorResidueEnergy Q q ≤ divisorResidueEnergy P q := by
…
```
Mentions: OAI.Problem337.divisorResidueEnergy