MomentRigidity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Numerical consequences of the actual moment exponents.

theorem OAI.CubicFirstMoment.first_shape_multiplicity_rigidity line 13

Source documentation

Rewriting the first configuration's sharp moment inequalities in terms of factor defects yields the manuscript's rigidity conclusion.

theorem first_shape_multiplicity_rigidity (a v : ι → ℝ) (r : ℝ)
    (ha : ∀ i, 0 ≤ a i ∧ a i < 1) (hsum : ∑ i, a i = 1)
    (hlarge : 7/3-2*(∑ i, v i) ≤ r)
    (hmoment : ∀ k : ι → ℕ,
      1/2 ≤ (∑ i, (k i:ℝ)*a i) → (∑ i, (k i:ℝ)*a i) ≤ 2 →
      r+2*(∑ i, (k i:ℝ)*v i) ≤ 2/3+(5/3)*(∑ i, (k i:ℝ)*a i)) :
    (∀ i, v i = 5*a i/6) ∧ r = 2/3 := by
…

theorem OAI.CubicFirstMoment.balanced_multiplicity_contradiction line 49

Source documentation

In the balanced configuration, the second moment lower bound and all actual fixed-copy ordinary moments contradict every factor having length exponent strictly below one.

theorem balanced_multiplicity_contradiction (a v : ι → ℝ) (r : ℝ)
    (ha : ∀ i, 0 ≤ a i ∧ a i < 1) (hv : ∀ i, v i ≤ a i)
    (hsum : ∑ i, a i = 1) (hlarge : 7/3-2*(∑ i, v i) ≤ r)
    (hcard : r ≤ 2/3)
    (hmoment : ∀ k : ι → ℕ, r+2*(∑ i, (k i:ℝ)*v i) ≤
      (∑ i, (k i:ℝ)*a i)+max (4/3) (∑ i, (k i:ℝ)*a i)) : False := by
…