OAI/Probability/GammaPassage/MeanNormSwap.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GammaFPP.rationalMean_swap line 10
2. lemma OAI.GammaFPP.realMeanExtension_swap line 17
3. lemma OAI.GammaFPP.gammaMeanPairSeminorm_swap line 32
4. theorem OAI.GammaFPP.gammaMeanNorm_swap line 46

   Source documentation

   Derived from actual expectation-limit symmetry through rational density.

   theorem gammaMeanNorm_swap (h : GammaEnvironment shape rate P τ)
       (hs : 0 < shape) (hr : 0 < rate) (v : Plane) :
       gammaMeanNorm h hs hr (Analytic.swapPlane v) = gammaMeanNorm h hs hr v := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.gammaMeanNorm, OAI.GammaFPP.Analytic.swapPlane