LocalComparisonInduction.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.CirculantHadamard.LocalComparison.isUnit_or_isUnit_of_mul_prime_unit line 21
Source documentation
If the product has exactly one prime factor up to a unit, at least one factor is a unit. This elementary base step does not use a valuation.
```
theorem isUnit_or_isUnit_of_mul_prime_unit {p x y : A} (hp : Prime p)
    (b : Aˣ) (hxy : x * y = p * (b : A)) : IsUnit x ∨ IsUnit y := by
…
```

theorem OAI.CirculantHadamard.LocalComparison.augmentation_ne_zero_of_scalar_product line 43

Source documentation

Both augmentations in the comparison theorem are nonzero.

theorem augmentation_ne_zero_of_scalar_product {p : ℕ} {e : ℕ}
    (hp : (p : A) ≠ 0) (b : Aˣ) (F K : Elem A (p ^ e))
    (hFK : F * K = scalar (p ^ e) ((p : A) ^ e * (b : A))) :
    augmentation (p ^ e) F ≠ 0 ∧ augmentation (p ^ e) K ≠ 0 := by
…

theorem OAI.CirculantHadamard.LocalComparison.comparison_base line 57

Source documentation

The exponent-one base case, using the actual residue field of S.

theorem comparison_base (n p : ℕ) (φ : A →+* S) (hp : Prime (p : A))
    (hpS : φ (p : A) ≠ 0)
    (v : Elem A n →+* S)
    (vscalar : ∀ a : A, v (scalar n a) = φ a)
    (vres : ∀ F : Elem A n,
      IsLocalRing.residue S (v F) =
        IsLocalRing.residue S (φ (augmentation n F)))
    (b : Aˣ) (F K : Elem A n)
    (hFK : F * K = scalar n ((p : A) * (b : A))) :
    ResidueOneAssociated (IsLocalRing.residue S) (v F) (φ (augmentation n F)) ∧
      ResidueOneAssociated (IsLocalRing.residue S) (v K) (φ (augmentation n K)) := by
…

Mentions: OAI.CirculantHadamard.LocalComparison.ResidueOneAssociated

theorem OAI.CirculantHadamard.LocalComparison.comparison_step_left line 94

Source documentation

Induction step when the first projected factor is divisible by p. The other factor is left intact. The two output associations are both transported, so the next step may divide either factor.

theorem comparison_step_left [IsDomain S] (p e : ℕ) (φ : A →+* S)
    (hp : (p : A) ≠ 0)
    (v : Elem A (p ^ (e + 1)) →+* S)
    (v' : Elem A (p ^ (e + 2)) →+* S)
    (vscalar : ∀ a : A, v (scalar (p ^ (e + 1)) a) = φ a)
    (vq : ∀ F : Elem A (p ^ (e + 2)),
      v (cyclicProjection A (pow_dvd_pow p (Nat.le_succ (e + 1))) F) = v' F)
    (b : Aˣ) (F K : Elem A (p ^ (e + 2)))
    (hFK : F * K = scalar (p ^ (e + 2)) ((p : A) ^ (e + 2) * (b : A)))
    (F' : Elem A (p ^ (e + 1)))
    (hF : cyclicProjection A (pow_dvd_pow p (Nat.le_succ (e + 1))) F =
      scalar (p ^ (e + 1)) (p : A) * F')
…

Mentions: OAI.CirculantHadamard.cyclicProjection

theorem OAI.CirculantHadamard.LocalComparison.comparison_induction line 135

Source documentation

The integral induction with its projection-divisibility input exposed. The concrete cyclotomic theorem discharges hdivide; it is not a definition of the comparison conclusion.

theorem comparison_induction (p : ℕ) (φ : A →+* S)
    (hp : Prime (p : A)) (hpS : φ (p : A) ≠ 0)
    (v : (e : ℕ) → Elem A (p ^ (e + 1)) →+* S)
    (vscalar : ∀ e a, v e (scalar (p ^ (e + 1)) a) = φ a)
    (vres : ∀ F : Elem A (p ^ 1),
      IsLocalRing.residue S (v 0 F) =
        IsLocalRing.residue S (φ (augmentation (p ^ 1) F)))
    (vq : ∀ e F,
      v e (cyclicProjection A (pow_dvd_pow p (Nat.le_succ (e + 1))) F) = v (e + 1) F)
    (hdivide : ∀ e (b : Aˣ) (F K : Elem A (p ^ (e + 2))),
      F * K = scalar (p ^ (e + 2)) ((p : A) ^ (e + 2) * (b : A)) →
      (∃ F', cyclicProjection A (pow_dvd_pow p (Nat.le_succ (e + 1))) F =
…