English
A generalization with null-measurable sets: volume of image equals volume divided by ENNReal.ofReal(covolume(L)).
Русский
Обобщение с нулевой измеряемостью: объём образа равен объёму, делённому на ENNReal.ofReal(коволюм(L)).
LaTeX
$$$\\operatorname{vol}\\big( (b.ofZLattice \\; \\mathbb{R} L)^{\\!\\mathrm{equivFun}}'' s \\big) = \\dfrac{\\operatorname{vol}(s)}{\\operatorname{ENNReal}.ofReal(\\operatorname{covolume}(L))}$$$
Lean4
theorem tendsto_card_le_div {X : Set (ι → ℝ)} (hX : ∀ ⦃x⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X) {F : (ι → ℝ) → ℝ}
(h₁ : ∀ x ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * (F x)) (h₂ : IsBounded ({x ∈ X | F x ≤ 1}))
(h₃ : MeasurableSet ({x ∈ X | F x ≤ 1})) (h₄ : volume (frontier {x | x ∈ X ∧ F x ≤ 1}) = 0) [Nonempty ι] :
Tendsto (fun c : ℝ ↦ Nat.card ({x ∈ X | F x ≤ c} ∩ L : Set (ι → ℝ)) / (c : ℝ)) atTop
(𝓝 (volume.real ({x ∈ X | F x ≤ 1}) / covolume L)) :=
by
classical
let e : Free.ChooseBasisIndex ℤ ↥L ≃ ι := by
refine Fintype.equivOfCardEq ?_
rw [← finrank_eq_card_chooseBasisIndex, ZLattice.rank ℝ, finrank_fintype_fun_eq_card]
let b := (Module.Free.chooseBasis ℤ L).reindex e
convert tendsto_card_le_div'' b hX h₁ h₂ h₃ ?_
· simp only [measureReal_def]
rw [volume_image_eq_volume_div_covolume L b, ENNReal.toReal_div, ENNReal.toReal_ofReal (covolume_pos L volume).le]
· rw [frontier_equivFun, volume_image_eq_volume_div_covolume, h₄, ENNReal.zero_div]
