OAI/NumberTheory/JointDickman/Amplification/LargeMultiplicityExponent.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.largeMultiplicityBase line 11
2. def OAI.JointDickman.largeMultiplicityLoss line 13
3. theorem OAI.JointDickman.largeMultiplicityBase_bounds line 16
4. theorem OAI.JointDickman.large_multiplicity_exponent_bound line 23

   Source documentation

   One old-coefficient choice at each endpoint and the opposite remainder's addition choices account for all three combinatorial entropy factors.

   theorem large_multiplicity_exponent_bound {g Δ δ τ ε ℓ : ℝ} {d f : ℕ}
       (hg : 0 ≤ g) (hg1 : g ≤ 1) (hδ : 0 ≤ δ) :
       largeAvailabilityExponent g Δ δ τ ε ℓ d+
         ((g/2)*Real.binEntropy (2*min ((d : ℝ)/(g*ℓ)) (1/2))+ε+highOmissionExponent τ)+
         ((g/2)*Real.binEntropy (2*min ((f : ℝ)/(g*ℓ)) (1/2))+ε+highOmissionExponent τ)+
         ((g/2)*Real.binEntropy (2*min ((f : ℝ)/(g*ℓ)) (1/2))+ε) ≤
           largeMultiplicityBase+largeMultiplicityLoss Δ δ τ ε := by
   …

   Mentions: OAI.JointDickman.largeAvailabilityExponent, OAI.JointDickman.highOmissionExponent, OAI.JointDickman.largeMultiplicityBase, OAI.JointDickman.largeMultiplicityLoss