OAI/Combinatorics/HoneycombChords/OrderedAssociation.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Ordered integral association and strip coefficient bounds

Formalized from Critical honeycomb chords with prescribed boundary endpoints (OpenAI, September 26, 2026).

  1. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.gramNodeDensity line 18
  2. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.errorNodeDensity line 21
  3. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ordered_eval_nonneg line 26
  4. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ordered_aug_zero_of_not_strict line 35
  5. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.nodeWeight_lattice line 44
  6. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.gramNodeDensity_lattice line 53
  7. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.gramNodeDensity_nonneg line 83
  8. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ordered_error_four_functions_pointwise line 91

    Source documentation

    A pointwise four-functions inequality for a cross-Gram ensemble with distinct left and right Chebyshev families.

    theorem ordered_error_four_functions_pointwise {n : ℕ} (F G : Fin n → ℝ → ℝ) (H w r : ℝ → ℝ)
    (hF : PositiveEvaluation F) (hG : PositiveEvaluation G)
    (hA : PositiveEvaluation (Fin.lastCases H F))
    (hcF : ∀ i,Continuous (F i)) (hcH : Continuous H)
    (hU : ∀ x,StrictMono x → (∀ i,0<x i) →
      0 ≤ (evaluationMatrix (Fin.lastCases H F) (Fin.cons 0 x)).det)
    (hw : ∀ p,0<p → 0 ≤ w p) (hr : ∀ p,0<p → 0 ≤ r p)
    (hm : MonotoneOn r (Set.Ioi 0))
    {x y : Fin n → ℝ} (hx : x∈orderedPositive n) (hy : y∈orderedPositive n) :
    errorNodeDensity F G H w x * gramNodeDensity F G (fun p ↦ w p*r p) y ≤
      gramNodeDensity F G w (x⊓y) * errorNodeDensity F G H (fun p ↦ w p*r p) (x⊔y) := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.w, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.PositiveEvaluation, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evaluationMatrix, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.errorNodeDensity, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.gramNodeDensity

  9. lemma OAI.Honeycomb370.orderedPositive_measurable line 162
  10. lemma OAI.Honeycomb370.unique_sorting_perm line 166
  11. lemma OAI.Honeycomb370.symmetric_ordered_indicator_sum line 181
  12. lemma OAI.Honeycomb370.integral_perm line 216
  13. theorem OAI.Honeycomb370.integral_symmetric_ordered line 224

    Source documentation

    The ordered chamber has exactly one representative of every noncollision orbit. The integrand vanishes on collision configurations.

    theorem integral_symmetric_ordered {n : ℕ} (f : (Fin n → ℝ) → ℝ)
    (hperm : ∀ x (σ : Perm (Fin n)),f (x ∘ σ)=f x)
    (hzero : ∀ x,¬Function.Injective x → f x=0)
    (hi : IntegrableOn f (orderedPositive n)) :
    (∫ x in Set.pi Set.univ (fun _ : Fin n ↦ Set.Ioi (0:ℝ)),f x)=
      (Fintype.card (Perm (Fin n)):ℝ)*(∫ x in orderedPositive n,f x) := by
…

    Mentions: OAI.Honeycomb370.orderedPositive

  14. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.gramNodeDensity_continuousOn line 252
  15. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.errorNodeDensity_continuousOn line 263
  16. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.errorNodeDensity_nonneg line 284
  17. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ordered_error_association line 299

    Source documentation

    Ordered association comparison for a nonsymmetric Gram ensemble with positive evaluations and integrable pairings.

    theorem ordered_error_association {n : ℕ} (F G : Fin n → ℝ → ℝ) (H w r : ℝ → ℝ)
    (hF : PositiveEvaluation F) (hG : PositiveEvaluation G)
    (hA : PositiveEvaluation (Fin.lastCases H F))
    (hcF : ∀ i,Continuous (F i)) (hcG : ∀ i,Continuous (G i)) (hcH : Continuous H)
    (hcw : ContinuousOn w (Set.Ioi 0)) (hcr : ContinuousOn r (Set.Ioi 0))
    (hU : ∀ x,StrictMono x → (∀ i,0<x i) →
      0 ≤ (evaluationMatrix (Fin.lastCases H F) (Fin.cons 0 x)).det)
    (hw : ∀ p,0<p → 0 ≤ w p) (hr : ∀ p,0<p → 0 ≤ r p)
    (hm : MonotoneOn r (Set.Ioi 0))
    (hi₁ : IntegrableOn (errorNodeDensity F G H w) (orderedPositive n))
    (hi₂ : IntegrableOn (gramNodeDensity F G (fun p ↦ w p*r p)) (orderedPositive n))
    (hi₃ : IntegrableOn (gramNodeDensity F G w) (orderedPositive n))
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.w, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.PositiveEvaluation, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evaluationMatrix, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.errorNodeDensity, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.gramNodeDensity

  18. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.power_det_nonneg_nonnegative line 338
  19. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.translated_kernel_minor_pair_nonneg line 354
  20. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.translated_kernel_det_nonneg line 382
  21. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.residual_det_augment_at line 414
  22. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyPointDensity_integrable_ordered line 451
  23. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyGram_ordered_integral line 460

    Source documentation

    Exact ordered Andreief identity for distinct left and right families.

    theorem familyGram_ordered_integral {n : ℕ} (w : ℝ → ℝ) (F G : Fin n → ℝ → ℝ)
    (hi : ∀ i j,IntegrableOn (fun p ↦ F i (p^2)*G j (p^2)*w p) (Set.Ioi 0)) :
    (∫ p in orderedPositive n,familyPointDensity w F G p)=(familyGram w F G).det := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.w, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyPointDensity, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyGram

  24. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.PositiveEvaluation.square line 482
  25. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.gramNodeDensity_square line 488
  26. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.errorNodeDensity_square line 493
  27. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.negative_meanResidualRatio_compare line 508

    Source documentation

    The actual negative coefficient can only increase when the weight is multiplied by an increasing ratio. Left and right systems are kept distinct.

    theorem negative_meanResidualRatio_compare (N : ℕ) (F G : Fin (2*N+1) → ℝ → ℝ)
    (H w r : ℝ → ℝ) (hF : PositiveEvaluation F) (hG : PositiveEvaluation G)
    (hA : PositiveEvaluation (Fin.lastCases H F))
    (hcF : ∀ i,Continuous (F i)) (hcG : ∀ i,Continuous (G i)) (hcH : Continuous H)
    (hcw : ContinuousOn w (Set.Ioi 0)) (hcr : ContinuousOn r (Set.Ioi 0))
    (hU : ∀ x,StrictMono x → (∀ i,0<x i) →
      0 ≤ (evaluationMatrix (Fin.lastCases H F) (Fin.cons 0 x)).det)
    (hw : ∀ p,0<p → 0 ≤ w p) (hr : ∀ p,0<p → 0 ≤ r p)
    (hm : MonotoneOn r (Set.Ioi 0)) (hH : 0<H 0)
    (hi : ∀ i j,IntegrableOn (fun p ↦ F i (p^2)*G j (p^2)*w p) (Set.Ioi 0))
    (hi' : ∀ i j,IntegrableOn (fun p ↦ F i (p^2)*G j (p^2)*(w p*r p)) (Set.Ioi 0))
    (hH₁ : ∀ j,IntegrableOn (fun p ↦ H (p^2)*G j (p^2)*w p) (Set.Ioi 0))
…

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

  28. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ratioP line 570
  29. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ratioQ line 571
  30. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ratioE line 572
  31. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sechRatio line 573
  32. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ratioP_pos line 576
  33. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ratioQ_pos line 579
  34. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ratioE_nonneg line 582
  35. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sechRatio_derivative line 586
  36. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sechRatio_monotone line 611
  37. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sinh_four line 623
  38. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.strip_sech_ratio_eq line 628
  39. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.strip_sech_ratio_monotone line 638

    Source documentation

    The ratio of the strip density to 1/cosh(3λp) is increasing for positive p.

    theorem strip_sech_ratio_monotone :
    MonotoneOn (fun p ↦ stripDensity p * Real.cosh (3*angle*p)) (Set.Ioi 0) := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripDensity, OAI.CriticalHoneycomb.FiniteFunctional.angle

  40. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.strip_coefficient_compare line 657
  41. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.mixedGram_ratio_le line 734
  42. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cThree_cosh_integrable line 759
  43. lemma OAI.CriticalHoneycomb.FiniteFunctional.strip_jet_coefficient_lower line 782
  44. theorem OAI.CriticalHoneycomb.FiniteFunctional.source_coefficient_inverse_sqrt line 793

    Source documentation

    A quantitative noncancellation bound for the mixed Gram coefficient.

    theorem source_coefficient_inverse_sqrt (N : ℕ) :
    1/(68*Real.pi*Real.sqrt ((N:ℝ)+1)) ≤ -(obliqueResidual N (C (3*angle/2)) 0).re := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.obliqueResidual, OAI.CriticalHoneycomb.FiniteFunctional.C, OAI.CriticalHoneycomb.FiniteFunctional.angle