OAI/NumberTheory/Ostmann/Construction/ConstituentEnergyTransport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.wordLeafAssignment_map line 12
2. def OAI.Ostmann.constituentWordLeafBase line 23
3. theorem OAI.Ostmann.constituent_wordLeaf_scale line 31
4. theorem OAI.Ostmann.constituent_energy_transport line 43

   Source documentation

   Fixing all other constituent primes and applying a uniform selected-leaf bound costs no factor. The measure is exactly the original product measure.

   theorem constituent_energy_transport {I D : Type*} [Fintype I] [Fintype D]
       (role : I → CopyScheduleRole) (size : I → ℕ)
       (i : Σ a, Fin (size a)) (hi : role i.1 = .word) (n : ℕ)
       (P : Finset ℕ) (cells : (Σ a, Fin (size a)) → Finset ℕ)
       (hsub : ∀ j, cells j ⊆ P) (hmass : ∀ j, (∑ p ∈ cells j, (p : ℝ)⁻¹) ≠ 0)
       (F : D → (CopyScheduleAtoms role n → ℕ) → ℝ) (B : ℝ)
       (hsection : ∀ base : CopyScheduleAtoms role n → ℕ,
         (∑ d, ∑ x : TreeLeafIndex n → P, (∏ t, primeSubsetPrior P (cells i) (x t)) *
           F d (wordLeafScale role i.1 hi n base (fun t => (x t : ℕ)))) ≤ B) :
       (∑ d, ∑ q : SurvivingConstituent role size n → P,
         scheduledPrimePrior (fun j : Σ a, Fin (size a) => role j.1) n
           (fun j => primeSubsetPrior P (cells j)) q *
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.primeSubsetPrior, OAI.Ostmann.wordLeafScale, OAI.Ostmann.SurvivingConstituent, OAI.Ostmann.scheduledPrimePrior