OAI/Combinatorics/HoneycombChords/SechResidual.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Polynomial generating functions and hyperbolic secant Gram residuals.

  1. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.alpha line 13
  2. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.A line 14
  3. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.w line 15
  4. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sec_pair_identity line 16
  5. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.alpha_pair_bound line 33
  6. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.A_sq line 39
  7. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.A_pair_integrable line 42
  8. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomial_generating_identity line 49
  9. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meanResidualRatio_coefficients line 84
  10. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cauchyGram_coefficient_lower line 102

    Source documentation

    Binding the explicit Cauchy model estimate to the actual nonsymmetric Gram projection. Its analytic realization is supplied by the sech transform.

    theorem cauchyGram_coefficient_lower (N : ℕ) (q : Fin (2*N) → ℝ) (u t : ℝ)
    (w : ℝ → ℝ) (F G : Fin (2*N+1) → ℝ → ℝ) (H : ℝ → ℝ)
    (hq : ∀ i,0≤q i ∧ q i≤1/2) (hu : 0≤u ∧ u≤1/2) (ht : 0≤t ∧ t≤1/2)
    (hinj : Function.Injective (Fin.lastCases t q))
    (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 : (familyGram w F G).det≠0)
    (hGram : ∀ i j,familyGram w F G i j=1/(1-Fin.lastCases u q i*Fin.lastCases t q j))
    (hMom : ∀ j,(∫ p in Set.Ioi 0,H (p^2)*G j (p^2)*w p)=1/(1-Fin.lastCases t q j))
    (hF0 : ∀ i,F i 0=1/Real.sqrt (1+Fin.lastCases u q i)) (hH0 : H 0=1/Real.sqrt 2) :
    1/(68*Real.pi*Real.sqrt ((N:ℝ)+1)) ≤ -(H 0*meanResidualRatio w F G H 0) := by
…

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

  11. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sechProbDensity line 139
  12. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.A_pair_prob_integrable line 141
  13. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.A_pair_prob_integral line 148
  14. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.alpha_mul_third line 158
  15. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.alpha_mul_half line 163
  16. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.w_bounds_third line 168
  17. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.A_zero line 190
  18. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.w_half line 201
  19. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.w_injectiveOn_third line 205
  20. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sech_label_margin line 230
  21. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sech_jet_pair_integrable line 245
  22. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sech_jet_gram_det_pos line 279
  23. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meanResidualRatio_reindex line 302
  24. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.residualFamily_scale_target line 310
  25. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meanResidualRatio_scale_target line 317
  26. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.finiteFamilyCombination_diagonal line 323
  27. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyGram_scalars line 328
  28. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meanResidualRatio_scalars line 335