OAI/NumberTheory/Ostmann/Construction/InitialBalancedCellWeights.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.balancedTupleSet_mass_one line 11
2. theorem OAI.Ostmann.exists_initial_balanced_cell_weights line 29

   Source documentation

   The additional top and compensation cells cost no balanced mass when all of their live primes were selected to be balanced. The two broad-shell cutoffs keep their original weights and their separate small centers.

   theorem exists_initial_balanced_cell_weights (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
       (b d r m : ℕ) (Tb Td : ℝ)
       (μb : Fin b → P → ℝ) (μd : Fin d → P → ℝ) (μc : Fin r → P → ℝ)
       (gb : Fin b → P → Prop) (gd : Fin d → P → Prop) (gc : Fin r → P → Prop)
       (hm : 1 ≤ m) (hb : b ≤ m) (hd : d ≤ m) (hTb : Tb ≤ m) (hTd : Td ≤ m)
       (hlogb : ∀ i (p : P), μb i p ≠ 0 → Real.log (p : ℝ) ≤ Real.exp Tb)
       (hlogd : ∀ i (p : P), μd i p ≠ 0 → Real.log (p : ℝ) ≤ Real.exp Td)
       (hmb : ∀ i, (1 / 2 : ℝ) ≤ ∑ p, if gb i p then μb i p else 0)
       (hmd : ∀ i, (1 / 2 : ℝ) ≤ ∑ p, if gd i p then μd i p else 0)
       (hmc : ∀ i, ∑ p, μc i p = 1)
       (hgc : ∀ i p, μc i p ≠ 0 → gc i p) :
       ∃ cb ∈ Finset.Icc (0 : ℤ) ⌈(b : ℝ) * Real.exp Tb⌉₊,
   …