OAI/Combinatorics/HoneycombChords/OrderedDeterminants.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Ordered determinant inequalities and positivity of the mixed interpolation family.

The development follows OpenAI, Uniform marked-polygon estimates and sharp finite bridge moments (2026), Sections 6 and 7.

  1. lemma OAI.Honeycomb370.det_two_update_one line 16
  2. lemma OAI.Honeycomb370.det_two_update_mulVec line 40
  3. lemma OAI.Honeycomb370.det_update_mulVec line 50
  4. theorem OAI.Honeycomb370.determinant_column_diamond line 58
  5. def OAI.Honeycomb370.mix line 88
  6. lemma OAI.Honeycomb370.mix_strictMono line 91
  7. lemma OAI.Honeycomb370.mix_le line 102
  8. lemma OAI.Honeycomb370.mix_zero line 110
  9. lemma OAI.Honeycomb370.mix_end line 114
  10. lemma OAI.Honeycomb370.mix_step line 118
  11. theorem OAI.Honeycomb370.monotone_ordered_of_coordinate line 129

    Source documentation

    Coordinatewise monotonicity on the ordered positive chamber.

    theorem monotone_ordered_of_coordinate {n : ℕ} (a : ℝ) (f : (Fin n → ℝ) → ℝ)
    (hlocal : ∀ x i r, (∀ k,a<x k) → StrictMono x → x i≤r →
      StrictMono (Function.update x i r) → f x≤f (Function.update x i r))
    {x y : Fin n → ℝ} (hxy : x≤y) (hxpos : ∀ k,a<x k)
    (hx : StrictMono x) (hy : StrictMono y) : f x≤f y := by
…
  12. theorem OAI.Honeycomb370.increasing_increment_ordered line 151

    Source documentation

    Increasing a single coordinate has a larger increment at a larger ordered base, provided all four ordered tuples are admissible.

    theorem increasing_increment_ordered {n : ℕ} (f : (Fin n → ℝ) → ℝ)
    (hlocal : ∀ (x : Fin n → ℝ) (i j : Fin n) (r s : ℝ), i ≠ j →
      x i ≤ r → x j ≤ s → (∀ k, 0 < x k) → StrictMono x →
      StrictMono (Function.update x i r) → StrictMono (Function.update x j s) →
      StrictMono (Function.update (Function.update x i r) j s) →
      f (Function.update x i r) + f (Function.update x j s) ≤
        f x + f (Function.update (Function.update x i r) j s))
    {x y : Fin n → ℝ} (i : Fin n) (r : ℝ)
    (hxy : x ≤ y) (hi : x i = y i) (hr : y i ≤ r)
    (hxpos : ∀ k, 0 < x k) (hx : StrictMono x) (hy : StrictMono y)
    (hxr : StrictMono (Function.update x i r))
    (hyr : StrictMono (Function.update y i r)) :
…
  13. theorem OAI.Honeycomb370.supermodular_ordered_of_local line 208

    Source documentation

    The exact global lattice inequality needed in the four-functions theorem. All inputs here are local two-coordinate inequalities, not association.

    theorem supermodular_ordered_of_local {n : ℕ} (f : (Fin n → ℝ) → ℝ)
    (hlocal : ∀ (x : Fin n → ℝ) (i j : Fin n) (r s : ℝ), i ≠ j →
      x i ≤ r → x j ≤ s → (∀ k, 0 < x k) → StrictMono x →
      StrictMono (Function.update x i r) → StrictMono (Function.update x j s) →
      StrictMono (Function.update (Function.update x i r) j s) →
      f (Function.update x i r) + f (Function.update x j s) ≤
        f x + f (Function.update (Function.update x i r) j s))
    {x y : Fin n → ℝ} (hxpos : ∀ k, 0 < x k) (hypos : ∀ k, 0 < y k)
    (hx : StrictMono x) (hy : StrictMono y) :
    f x + f y ≤ f (x ⊓ y) + f (x ⊔ y) := by
…
  14. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyCombination line 282
  15. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.PositiveFlag line 284
  16. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyTestCoeffs line 286
  17. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyTest_eq_det line 288
  18. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.monomial_positiveEvaluation line 296
  19. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyTest_sign_product line 301
  20. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyCombination_smul line 319
  21. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyCombination_continuous line 325
  22. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.positive_flag_sign_matching line 329
  23. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.vandermonde_local_logsupermodular line 381
  24. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.eval_update line 406
  25. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.eval_det_zero_of_noninjective line 412
  26. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.positiveEvaluation_local_logsupermodular line 420
  27. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.positiveEvaluation_logsupermodular line 472

    Source documentation

    Ordered-node MTP2 for a genuine (not necessarily polynomial) positive Chebyshev evaluation determinant.

    theorem positiveEvaluation_logsupermodular {n : ℕ} (F : Fin n → ℝ → ℝ)
    (hF : PositiveEvaluation F) {x y : Fin n → ℝ}
    (hx0 : ∀ i, 0 < x i) (hy0 : ∀ i, 0 < y i)
    (hx : StrictMono x) (hy : StrictMono y) :
    (evaluationMatrix F x).det * (evaluationMatrix F y).det ≤
      (evaluationMatrix F (x ⊓ y)).det * (evaluationMatrix F (x ⊔ y)).det := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.PositiveEvaluation, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evaluationMatrix

  28. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.centralIndex line 538
  29. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.fixedFamily line 539
  30. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.realG line 542
  31. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.mixedFamily line 543
  32. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.realG_complex line 546
  33. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.fixedFamily_central line 549
  34. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.fixedFamily_eq_interior_away line 554
  35. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.fixedFamily_update_interior line 563
  36. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rowDetLinear line 575
  37. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rowDet_integral line 581
  38. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evaluationMatrix_update line 594
  39. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.fixedFamily_positiveEvaluation line 607
  40. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.mixedFamily_positiveEvaluation line 613
  41. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.realG_sq line 658
  42. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.realG_sq_nonneg line 662
  43. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.realG_sq_le line 666
  44. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jet_realG_pair_integrable line 680
  45. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.fixedFamily_pair_integrable line 702
  46. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.fixed_mixed_pair_integrable line 710
  47. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.fixed_mixed_Gram_det_pos line 723

    Source documentation

    The nonsymmetric pairing matrix in the precise F0 and G spaces is invertible. This follows from its positive determinant, not from symmetry.

    theorem fixed_mixed_Gram_det_pos (N : ℕ) :
    0 < (familyGram stripDensity (fixedFamily N) (mixedFamily N)).det :=
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyGram, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripDensity, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.fixedFamily, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.mixedFamily