English
The absolute determinant identity for fderiv_expMapBasis holds in the alternate expression.
Русский
Стержневая формула модуля детерминанта для fderiv_expMapBasis в другой форме.
LaTeX
$$abs((fderiv_expMapBasis K x).det) = ...$$
Lean4
theorem setLIntegral_paramSet_exp {n : ℕ} (hn : 0 < n) :
∫⁻ (x : realSpace K) in paramSet K, .ofReal (Real.exp (x w₀ * n)) = (n : ℝ≥0∞)⁻¹ := by
classical
have hn : 0 < (n : ℝ) := Nat.cast_pos.mpr hn
rw [volume_pi, paramSet, Measure.restrict_pi_pi, lintegral_eq_lmarginal_univ 0,
lmarginal_erase' _ (by fun_prop) (Finset.mem_univ w₀), if_pos rfl]
simp_rw [Function.update_self, lmarginal, lintegral_const, Measure.pi_univ,
if_neg (Finset.ne_of_mem_erase (Subtype.prop _)), Measure.restrict_apply_univ, Real.volume_Ico, sub_zero,
ofReal_one, prod_const_one, mul_one, mul_comm _ (n : ℝ)]
rw [← ofReal_integral_eq_lintegral_ofReal (integrableOn_exp_mul_Iic hn _), integral_exp_mul_Iic hn, mul_zero,
Real.exp_zero, ofReal_div_of_pos hn, ofReal_one, ofReal_natCast, one_div]
filter_upwards with _ using Real.exp_nonneg _
