OAI/Analysis/LiebThirring/ExtremizerMass.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpLiebThirring.ExtremizerProof.potential_power_integral line 12

   Source documentation

   Exact substitution z = tanh (r*x); no integrability convention is used to guess the integral, since the Jacobian theorem applies to the full line.

   lemma potential_power_integral {r σ : ℝ} (hr : 0 < r) :
       (∫ x, (potential r x)^(1+σ)) = (r+1)^(1+σ)/r * betaAction σ := by
   …

   Mentions: OAI.SharpLiebThirring.ExtremizerProof.potential

2. lemma OAI.SharpLiebThirring.ExtremizerProof.young_times_extremizer_factor line 56
3. lemma OAI.SharpLiebThirring.ExtremizerProof.sharp_times_extremizer_integral line 66