OAI/NumberTheory/Ostmann/Arithmetic/MovingOriginalPatternMean.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingOriginalPairPrimeKernel line 14

   Source documentation

   The fixed-sample prime integral before choosing any equality pattern.

   noncomputable def movingOriginalPairPrimeKernel {σ I B : Type} {n : ℕ}
       (q : I → ℕ) [∀ i, Fact (q i).Prime] (value : σ → ℕ) (outside : List ℕ)
       (childBound pivotBound : ℕ → ℕ)
       (F : {d : ℕ} → MovingSlotData σ d → ℤ → ℂ)
       (g : ∀ i, ZMod (q i) → ℂ) (Dq : ∀ i, (ZMod (q i))ˣ) (S : Finset I)
       (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ) (φ : ℝ → ℝ) (G : ℕ → ℝ)
       (t : Bool → FrequencyTree ℤ n) (small bulk : TreeLeafTuple (List B) n)
       (u v r w : ℝ) (y : B → σ) (a : MovingSampleSlots σ n × MovingSampleSlots σ n) : ℂ :=
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots

2. def OAI.Ostmann.movingOriginalPatternPrimeObservable line 32

   Source documentation

   The same actual prime integral in the full finite pattern coordinates.

   noncomputable def movingOriginalPatternPrimeObservable {σ I B C : Type}
       {N n : ℕ} (e : Fin (N + 1) ≃ B ⊕ C)
       (pattern : Bool × MovingSampleIndex n → C)
       (q : I → ℕ) [∀ i, Fact (q i).Prime] (value : σ → ℕ) (outside : List ℕ)
       (childBound pivotBound : ℕ → ℕ)
       (F : {d : ℕ} → MovingSlotData σ d → ℤ → ℂ)
       (g : ∀ i, ZMod (q i) → ℂ) (Dq : ∀ i, (ZMod (q i))ˣ) (S : Finset I)
       (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ) (φ : ℝ → ℝ) (G : ℕ → ℝ)
       (t : Bool → FrequencyTree ℤ n) (small bulk : TreeLeafTuple (List B) n)
       (u v r w : ℝ) (x : Fin (N + 1) → σ) : ℂ :=
   …

   Mentions: OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.MovingSlotData, OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple

3. theorem OAI.Ostmann.moving_external_pattern_mean line 47

   Source documentation

   Finite reindexing is proved independently of the large prime integrand.

   theorem moving_external_pattern_mean {σ B : Type} [Fintype σ] [Fintype B]
       (μ : ℕ → σ → ℝ) (ν : B → σ → ℝ) (value : σ → ℕ) (n : ℕ)
       (H : (B → σ) → (MovingSampleSlots σ n × MovingSampleSlots σ n) → ℂ) :
       let _ := sampleSetoidFintype (Bool × MovingSampleIndex n)
   …

   Mentions: OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.sampleSetoidFintype, OAI.Ostmann.MovingSampleIndex

4. theorem OAI.Ostmann.movingOriginalPrimePairMean_patterns line 88

   Source documentation

   Exact passage from the original two-history mean to the full coordinate sum used by the arithmetic comparison. No independence of repeated internal samples, deleted prime law, or new normalization is introduced.

   theorem movingOriginalPrimePairMean_patterns {σ I B : Type}
       [Fintype σ] [Fintype B]
       (q : I → ℕ) [∀ i, Fact (q i).Prime] (value : σ → ℕ) (outside : List ℕ)
       (μ : ℕ → σ → ℝ) (ν : B → σ → ℝ) (childBound pivotBound : ℕ → ℕ)
       (F : {n : ℕ} → MovingSlotData σ n → ℤ → ℂ)
       (g : ∀ i, ZMod (q i) → ℂ) (Dq : ∀ i, (ZMod (q i))ˣ) (S : Finset I)
       (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ) (φ : ℝ → ℝ) (G : ℕ → ℝ)
       (n : ℕ) (t : Bool → FrequencyTree ℤ n) (small bulk : TreeLeafTuple (List B) n)
       (u v r w : ℝ) :
       let _ := sampleSetoidFintype (Bool × MovingSampleIndex n)
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.sampleSetoidFintype, OAI.Ostmann.MovingSampleIndex