OAI/NumberTheory/Ostmann/Arithmetic/MovingAuxiliaryUnits.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingAuxiliaryLocalUnits line 10
2. def OAI.Ostmann.movingAuxiliaryUnits line 15
3. theorem OAI.Ostmann.movingNaturalGiantUnits_auxiliary line 23
4. theorem OAI.Ostmann.localGiantUnits_of_pairwise line 32
5. theorem OAI.Ostmann.movingFullOutsidePairwise_giantUnits line 40
6. theorem OAI.Ostmann.movingFullSupport_auxiliary_iff line 50
7. theorem OAI.Ostmann.currentOutsidePairwise_auxiliary_iff line 57
8. theorem OAI.Ostmann.movingFullOutsidePairwise_auxiliary_iff line 74
9. theorem OAI.Ostmann.naturalProduct_coprime_of_members line 87
10. theorem OAI.Ostmann.movingAuxiliaryUnits_cross line 96
11. theorem OAI.Ostmann.movingFullSupport_auxiliary_square_iff line 118

    Source documentation

    All descendant regular-slot units have disappeared; only the top current pair, the explicit square tests, and frequency/outside tests remain.

    theorem movingFullSupport_auxiliary_square_iff {σ : Type*} (value : σ → ℕ) (outside : List ℕ)
        {n : ℕ} (T : MovingSlotData σ n) (hcoh : T.RegularCoherent) (hc : T.CompensationPrimeData value)
        (hsmall : ∀ i, T.Frequencies (fun s => IsCoprime s (value i : ℤ))) (XL XR : ℕ)
        (hI : T.Integral value XL XR) :
        movingFullSupport value outside T XL XR ↔
          T.CurrentPairwise value XL XR ∧ movingRegularOutsidePairwise value outside T ∧
            T.PrimeSquareTests value XL XR ∧ movingAuxiliaryUnits value outside T XL XR := by
    …

    Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingFullSupport, OAI.Ostmann.movingRegularOutsidePairwise, OAI.Ostmann.movingAuxiliaryUnits