OAI/Combinatorics/HoneycombChords/LaplaceProfile.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Scalar Laplace profile estimates

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

  1. def OAI.CriticalHoneycomb.RenewalInput.laplaceProfile line 18

    Source documentation

    Scalar comparison used in the actual bridge renewal transform.

    noncomputable def laplaceProfile (s x : ℝ) : ℝ :=
…
  2. lemma OAI.CriticalHoneycomb.RenewalInput.laplaceProfile_pos line 21
  3. lemma OAI.CriticalHoneycomb.RenewalInput.laplaceProfile_antitone line 25
  4. lemma OAI.CriticalHoneycomb.RenewalInput.laplaceProfile_continuous line 34
  5. lemma OAI.CriticalHoneycomb.RenewalInput.gammaProfile_integral line 38
  6. lemma OAI.CriticalHoneycomb.RenewalInput.gammaProfile_integrable line 47
  7. lemma OAI.CriticalHoneycomb.RenewalInput.laplaceProfile_integrable line 55
  8. lemma OAI.CriticalHoneycomb.RenewalInput.laplaceProfile_summable line 63
  9. lemma OAI.CriticalHoneycomb.RenewalInput.laplaceProfile_integral_le line 68
  10. lemma OAI.CriticalHoneycomb.RenewalInput.laplaceProfile_sum_upper line 76
  11. lemma OAI.CriticalHoneycomb.RenewalInput.laplaceProfile_sum_lower line 86