OAI/NumberTheory/Ostmann/Arithmetic/RealBulkKernel.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.realValueFullSupport line 14
2. def OAI.Ostmann.realValueSupportFlag line 20
3. def OAI.Ostmann.realValueKernel line 25
4. theorem OAI.Ostmann.realValueSupportFlag_norm line 32
5. theorem OAI.Ostmann.realValueSupportFlag_nat line 39

   Source documentation

   The real extension has precisely the old arithmetic gates and windows.

   theorem realValueSupportFlag_nat {σ : Type*} (value : σ → ℕ) (hv : ∀ i, value i ≠ 0)
       (childBound pivotBound : ℕ → ℕ) {n : ℕ} (T : MovingSlotData σ n)
       (hf : T.Frequencies (· ≠ 0)) (X lo hi L R : ℝ) :
       realValueSupportFlag (fun i => (value i : ℝ)) childBound pivotBound T X lo hi L R =
         movingRealGateWeight value T
           (T.formulaNodes value hv childBound pivotBound hf (.prime false) (.prime true))
           X lo hi (topGiantReal L R) := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.realValueSupportFlag, OAI.Ostmann.movingRealGateWeight, OAI.Ostmann.topGiantReal

6. theorem OAI.Ostmann.realValueKernel_nat line 55
7. theorem OAI.Ostmann.MovingSlotReversal.continuous_bulkLogComposite line 67
8. theorem OAI.Ostmann.isClosed_bulkLogNodeSupport line 77
9. theorem OAI.Ostmann.isClosed_bulkLogFullSupport line 94
10. theorem OAI.Ostmann.measurable_bulkLogKernel line 106
11. theorem OAI.Ostmann.realValueKernel_norm line 124
12. def OAI.Ostmann.bulkLogKernelIntegrand line 139