OAI/Combinatorics/HoneycombChords/FamilyGram.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

Positive function families, Gram compression, basis changes, and knot continuity.

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

  1. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroJetLift line 14
  2. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroJetLift_eq line 16
  3. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroJetLift_ne_zero line 22
  4. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroJetCombination_zero line 27
  5. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroJetCombination_continuous line 29
  6. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroJetCombination_zeros_card_lt line 34
  7. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroJetCombination_finite_zeros line 47
  8. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroJetEvaluation line 54
  9. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroJetEvaluation_det line 56
  10. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroJetEvaluation_det_pos line 80
  11. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.PositiveEvaluation line 102

    Source documentation

    Positivity of the actual ordered evaluation determinant. Used below for both regular and zero-at-origin jet bases, including the mixed second chain.

    def PositiveEvaluation {n : ℕ} (F : Fin n → ℝ → ℝ) : Prop :=
…
  12. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evaluation_det_product_pos line 104
  13. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evaluation_det_product_nonneg line 121
  14. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jet_positiveEvaluation line 132
  15. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroJet_positiveEvaluation line 137
  16. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyGram line 150
  17. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyPointDensity line 153
  18. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.weighted_family_evaluation line 155
  19. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.family_gram_andreief line 165
  20. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyPointDensity_pos line 190
  21. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyGram_det_pos line 201
  22. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.determinant_quotient_of_quadratic_bounds line 256

    Source documentation

    Quadratic-form bounds give determinant bounds with the exact dimension. This is the finite-dimensional stability estimate required in the polynomial compression step of strip-asymptotics.tex:83--84.

    theorem determinant_quotient_of_quadratic_bounds {n : ℕ}
    (A B : Matrix (Fin n) (Fin n) ℝ) (hA:A.IsHermitian) (hB:B.PosDef)
    {l u:ℝ} (hl:0≤l)
    (hlo:∀ v:Fin n→ℝ,l*(v ⬝ᵥ (B *ᵥ v))≤v ⬝ᵥ (A *ᵥ v))
    (hup:∀ v:Fin n→ℝ,v ⬝ᵥ (A *ᵥ v)≤u*(v ⬝ᵥ (B *ᵥ v))) :
    l^n≤A.det/B.det ∧ A.det/B.det≤u^n := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.A

  23. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.determinant_mono_of_positive_base line 287

    Source documentation

    Loewner monotonicity of determinant, with a positive definite base.

    theorem determinant_mono_of_positive_base {n:ℕ}
    (A B:Matrix (Fin n) (Fin n) ℝ) (hA:A.IsHermitian) (hB:B.PosDef)
    (h:∀ v:Fin n→ℝ,v ⬝ᵥ (B *ᵥ v)≤v ⬝ᵥ (A *ᵥ v)) : B.det≤A.det := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.A

  24. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.small_error_power_bounds line 320
  25. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.determinant_small_relative_error line 335

    Source documentation

    Uniform constant-factor determinant stability requires dimension times quadratic error to be small; this factor cannot be omitted.

    theorem determinant_small_relative_error {n:ℕ}
    (A D:Matrix (Fin n) (Fin n) ℝ) (hA:A.PosDef) (hD:D.IsHermitian)
    {η:ℝ} (hη:0≤η) (hη1:η≤1/2) (hn:(n:ℝ)*η≤1/2)
    (herr:∀ v:Fin n→ℝ,|v ⬝ᵥ (D *ᵥ v)-v ⬝ᵥ (A *ᵥ v)|≤η*(v ⬝ᵥ (A *ᵥ v))) :
    (1:ℝ)/2≤D.det/A.det ∧ D.det/A.det≤2 := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.A, OAI.CriticalHoneycomb.FiniteFunctional.D

  26. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.gram_quotient_small_relative_error line 347
  27. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rectangular_diagonal_gram_det line 391
  28. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.diagonal_compression_det_lower line 424
  29. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.positive_contraction_compression line 452

    Source documentation

    Compression to any finite subspace increases the determinant of a positive contraction. The Gram quotient makes the statement independent of the basis.

    theorem positive_contraction_compression {n m:ℕ}
    (A B:Matrix (Fin m) (Fin m) ℝ) (C:Matrix (Fin n) (Fin m) ℝ)
    (hA:A.PosDef) (hB:B.PosDef) (hCB:(C*B*Cᵀ).PosDef)
    (hAB:∀ v:Fin m→ℝ,v ⬝ᵥ (A *ᵥ v)≤v ⬝ᵥ (B *ᵥ v)) :
    A.det/B.det≤(C*A*Cᵀ).det/(C*B*Cᵀ).det := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.A, OAI.CriticalHoneycomb.FiniteFunctional.C

  30. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.finiteFamilyCombination line 508
  31. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familySquaredNorm line 509
  32. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.finiteFamilyCombination_pair_integrable line 510
  33. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyGram_congruence line 525
  34. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyGram_quad line 551
  35. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyGram_hermitian line 570
  36. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familySquaredNorm_nonneg line 577
  37. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familySquaredNorm_error_bound line 581
  38. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.residualFamily line 619

    Source documentation

    Evaluation rows with the rank-one interpolation correction.

    noncomputable def residualFamily {n : ℕ} (F : Fin n → ℝ → ℝ) (H : ℝ → ℝ) (a : ℝ) :
    Fin n → ℝ → ℝ := fun i x=>F i x-F i a*H x/H a
  39. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meanResidualRatio line 621
  40. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.residualFamily_pair_integrable line 625
  41. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.residualFamily_gram line 636
  42. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.det_sub_vecMulVec line 652
  43. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meanResidualRatio_formula line 666
  44. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meanResidualRatio_eq_integral line 678
  45. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyPointDensity_tilt line 691
  46. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meanResidualRatio_bound line 698

    Source documentation

    Transfer any pointwise residual bound to the exact determinant averages.

    lemma meanResidualRatio_bound {n : ℕ} (w w₁ w₂ : ℝ → ℝ) (F G : Fin n → ℝ → ℝ)
    (H : ℝ → ℝ) (a A B : ℝ)
    (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) (Set.Ioi 0))
    (hi₂ : ∀ i j,IntegrableOn (fun p=>F i (p^2)*G j (p^2)*w₂ p) (Set.Ioi 0))
    (hH : ∀ j,IntegrableOn (fun p=>H (p^2)*G j (p^2)*w p) (Set.Ioi 0))
    (hd : 0<(familyGram w F G).det)
    (hb : ∀ p : Fin n → ℝ,(∀ i,0<p i) →
      familyPointDensity w (residualFamily F H a) G p ≤
        A*familyPointDensity w₁ F G p+B*familyPointDensity w₂ F G p) :
    meanResidualRatio w F G H a ≤
      A*((familyGram w₁ F G).det/(familyGram w F G).det)+
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.w, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.A, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyGram, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyPointDensity, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.residualFamily, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meanResidualRatio

  47. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newton_pair_integrable line 745
  48. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.tendsto_newton_pair_integral line 766
  49. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyGram_left_combination line 809
  50. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyGram_right_combination line 825
  51. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.combination_pair_integrable_left line 841
  52. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyGram_bichange line 852
  53. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.residualFamily_combination line 860
  54. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meanResidualRatio_bichange line 870
  55. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jet_meanResidualRatio_eq_newton line 893
  56. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.tendsto_newton_meanResidualRatio line 917
  57. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.commonApproach line 983
  58. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.interiorApproach line 985
  59. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.commonApproach_low line 988
  60. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.commonApproach_high line 997
  61. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.commonApproach_bounds line 1007
  62. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.commonApproach_strictMono line 1014
  63. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.interiorApproach_bounds line 1033
  64. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.interiorApproach_strictMono line 1039
  65. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.nodalOrder_eq_zero_of_strictMono_prefix line 1065
  66. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.interiorApproach_permutation line 1074
  67. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.tendsto_commonApproach line 1086
  68. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.tendsto_interiorApproach line 1096