OAI/Combinatorics/HoneycombChords/SechExpectation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Normalized expectation for the hyperbolic secant measure.

  1. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sechExpectation line 12

    Source documentation

    The probability average under dp/cosh(cp), pushed forward by p ↦ p². The transform below also proves its normalization.

    noncomputable def sechExpectation (c : ℝ) (H : ℝ → ℝ) : ℝ :=
…
  2. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sechExpectation_one line 14