OAI/Combinatorics/HoneycombChords/BetaKernel.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Calculus, total positivity, and exponential bounds for the entire beta kernel.

  1. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet_zero_zero_cos line 11
  2. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomialJet_at_zero_X_pow line 23
  3. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet_at_zero line 26
  4. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet_contDiff_right line 34
  5. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet_contDiff_left line 47
  6. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.complete_beta_jet_det_pos line 51

    Source documentation

    The complete jet determinant with literal iterated derivatives, not a series interface.

    lemma complete_beta_jet_det_pos {n : ℕ} (b x : ℕ → ℝ)
    (hb : Monotone (fun i : Fin n=>b i)) (hx : Monotone (fun i : Fin n=>x i))
    (hb0 : ∀ i : Fin n,0 ≤ b i) (hx0 : ∀ i : Fin n,0 ≤ x i) :
    0 < Matrix.det (fun i j : Fin n=>iteratedDeriv (nodalOrder x j)
      (fun y=>iteratedDeriv (nodalOrder b i) (fun z=>cosineKernelJet 0 0 z y) (b i)) (x j)) := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.nodalOrder, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet

  7. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.binomial_term_le_add_pow line 76
  8. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet_nonneg line 84
  9. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet_label_bound line 90
  10. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet_exp_bound line 105