OAI/NumberTheory/Ostmann/Arithmetic/MovingRealWeight.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingRealWeight line 12

   Source documentation

   Real evaluation of the very same moving recursion, before arithmetic indicators. The reciprocal compensation product remains in every pivot.

   noncomputable def movingRealWeight {σ : Type*} (value : σ → ℕ)
       (F : ∀ {n}, MovingSlotData σ n → ℝ → ℝ → ℂ)
       (E : ∀ {n}, MovingSlotData σ n → ℝ → ℝ → ℝ) :
       {n : ℕ} → MovingSlotData σ n → ℝ → ℝ → ℂ
     | _, .leaf s regular, L, R => F (.leaf s regular) L R
     | _, .node s CL CR u left right, L, R =>
         let p := (MovingSlotData.step s CL CR u left right false).realPivot value L R
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.MovingSlotData.step

2. def OAI.Ostmann.movingRealLeaf line 22
3. def OAI.Ostmann.movingRealExtra line 26
4. theorem OAI.Ostmann.movingRealWeight_eq_unrestricted line 33

   Source documentation

   Agreement uses the proved integer recursion, not a new realization hypothesis for each of the polynomial leaves.

   theorem movingRealWeight_eq_unrestricted {σ : Type*} (value : σ → ℕ)
       (hvalue : ∀ i, value i ≠ 0)
       (F : ∀ {n}, MovingSlotData σ n → ℝ → ℝ → ℂ)
       (E : ∀ {n}, MovingSlotData σ n → ℝ → ℝ → ℝ)
       {n : ℕ} (T : MovingSlotData σ n) (hf : T.Frequencies (· ≠ 0))
       (XL XR : ℕ) (hI : T.Integral value XL XR) :
       movingRealWeight value F E T XL XR =
         movingUnrestrictedWeight value (movingRealLeaf F) (movingRealExtra E) T XL XR := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingRealWeight, OAI.Ostmann.movingUnrestrictedWeight, OAI.Ostmann.movingRealLeaf, OAI.Ostmann.movingRealExtra

5. theorem OAI.Ostmann.movingSlotWeight_real_factor line 53

   Source documentation

   Exact smooth/arithmetic separation for the original recursive weight. All invalid integer reconstructions are retained as zero terms.

   theorem movingSlotWeight_real_factor {σ : Type*} (value : σ → ℕ)
       (hvalue : ∀ i, value i ≠ 0) (childBound pivotBound : ℕ → ℕ)
       (F : ∀ {n}, MovingSlotData σ n → ℝ → ℝ → ℂ)
       (E : ∀ {n}, MovingSlotData σ n → ℝ → ℝ → ℝ)
       {n : ℕ} (T : MovingSlotData σ n) (t : FrequencyTree ℤ n) (hT : T.Follows t)
       (hf : T.Frequencies (· ≠ 0)) (XL XR : ℕ) :
       recursiveTransferWeight (movingSlotSystem value childBound pivotBound) (movingRealLeaf F)
         (movingSlotCutoff value childBound pivotBound (movingRealExtra E)) n ⟨n, T, XL, XR⟩ t =
           movingArithmeticIndicator value childBound pivotBound T XL XR *
             movingRealWeight value F E T XL XR := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.FrequencyTree, OAI.Ostmann.recursiveTransferWeight, OAI.Ostmann.movingSlotSystem, OAI.Ostmann.movingRealLeaf, OAI.Ostmann.movingSlotCutoff, OAI.Ostmann.movingRealExtra, OAI.Ostmann.movingArithmeticIndicator, OAI.Ostmann.movingRealWeight

6. theorem OAI.Ostmann.movingSlotWeight_real_cell_difference line 71

   Source documentation

   Once the indicator is fixed on a residue/root cell, its contribution to an oscillation is at most that of the explicit real weight.

   theorem movingSlotWeight_real_cell_difference {σ : Type*} (value : σ → ℕ)
       (hvalue : ∀ i, value i ≠ 0) (childBound pivotBound : ℕ → ℕ)
       (F : ∀ {n}, MovingSlotData σ n → ℝ → ℝ → ℂ)
       (E : ∀ {n}, MovingSlotData σ n → ℝ → ℝ → ℝ)
       {n : ℕ} (T : MovingSlotData σ n) (t : FrequencyTree ℤ n) (hT : T.Follows t)
       (hf : T.Frequencies (· ≠ 0)) (XL YL XR : ℕ)
       (hres : (XL : ℤ) ≡ (YL : ℤ) [ZMOD movingTopPeriod value hvalue childBound pivotBound T hf])
       (hcell : rootCellCode (movingTopRootCuts value hvalue childBound pivotBound T hf XR) (XL : ℝ) =
         rootCellCode (movingTopRootCuts value hvalue childBound pivotBound T hf XR) (YL : ℝ)) :
       ‖recursiveTransferWeight (movingSlotSystem value childBound pivotBound) (movingRealLeaf F)
           (movingSlotCutoff value childBound pivotBound (movingRealExtra E)) n ⟨n, T, XL, XR⟩ t -
         recursiveTransferWeight (movingSlotSystem value childBound pivotBound) (movingRealLeaf F)
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.FrequencyTree, OAI.Ostmann.movingTopPeriod, OAI.Ostmann.rootCellCode, OAI.Ostmann.movingTopRootCuts, OAI.Ostmann.recursiveTransferWeight, OAI.Ostmann.movingSlotSystem, OAI.Ostmann.movingRealLeaf, OAI.Ostmann.movingSlotCutoff, OAI.Ostmann.movingRealExtra