OAI/NumberTheory/Ostmann/Arithmetic/MovingDiagonalOuterWeight.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.inactiveRegularDensity line 11
2. theorem OAI.Ostmann.inactiveRegularDensity_bounds line 15
3. theorem OAI.Ostmann.inactiveRegularDensity_joinBulkNonbulk line 32

   Source documentation

   Inactive factors use only the fixed nonbulk coordinates.

   theorem inactiveRegularDensity_joinBulkNonbulk {A σ J K : Type*} [Fintype J]
       (prime : A → ℕ) (reg : J → σ) (active : J → Bool) (slot : K ↪ σ)
       (hfixed : ∀ j, active j = false → reg j ∉ Set.range slot)
       (x : σ → A) (z : K → A) :
       inactiveRegularDensity prime reg active (joinBulkNonbulk slot z (fun i => x i)) =
         inactiveRegularDensity prime reg active x := by
   …

   Mentions: OAI.Ostmann.inactiveRegularDensity, OAI.Ostmann.joinBulkNonbulk

4. def OAI.Ostmann.diagonalOuterMajorant line 47
5. theorem OAI.Ostmann.diagonalOuterMajorant_pos line 51
6. def OAI.Ostmann.movingDiagonalOuterWeight line 60
7. theorem OAI.Ostmann.movingDiagonalOuterWeight_norm line 68
8. theorem OAI.Ostmann.movingDiagonalOuterWeight_measurable line 90
9. theorem OAI.Ostmann.movingDiagonalOuterWeight_bulk line 102