tendsto_addHaar_inter_smul_zero_of_density_zero_aux1

English

Given ω an alternating map on G and a basis b, the measure ω.measure of parallelepiped equals ENNReal.ofReal(abs det ω).

Русский

Для ω чередующейся отображения на G и базиса b мера ω.measure параллелепипеда равна ENNReal.ofReal(abs det ω).

LaTeX

$$$\omega.measure(\text{parallelepiped}(v)) = ENNReal.ofReal|\omega v|$$$

Lean4

theorem tendsto_addHaar_inter_smul_zero_of_density_zero_aux1 (s : Set E) (x : E)
    (h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)) (t : Set E) (u : Set E)
    (h'u : μ u ≠ 0) (t_bound : t ⊆ closedBall 0 1) :
    Tendsto (fun r : ℝ => μ (s ∩ ({ x } + r • t)) / μ ({ x } + r • u)) (𝓝[>] 0) (𝓝 0) :=
  by
  have A : Tendsto (fun r : ℝ => μ (s ∩ ({ x } + r • t)) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0) :=
    by
    apply tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds h (Eventually.of_forall fun b => zero_le _)
    filter_upwards [self_mem_nhdsWithin]
    rintro r (rpos : 0 < r)
    grw [t_bound]
    rw [← vadd_eq_add, singleton_vadd, affinity_unitClosedBall rpos.le]
  have B :
    Tendsto (fun r : ℝ => μ (closedBall x r) / μ ({ x } + r • u)) (𝓝[>] 0) (𝓝 (μ (closedBall x 1) / μ ({ x } + u))) :=
    by
    apply tendsto_const_nhds.congr' _
    filter_upwards [self_mem_nhdsWithin]
    rintro r (rpos : 0 < r)
    have : closedBall x r = { x } + r • closedBall (0 : E) 1 := by
      simp only [_root_.smul_closedBall, Real.norm_of_nonneg rpos.le, zero_le_one, add_zero, mul_one,
        singleton_add_closedBall, smul_zero]
    simp only [this, addHaar_singleton_add_smul_div_singleton_add_smul μ rpos.ne']
    simp only [addHaar_closedBall_center, image_add_left, measure_preimage_add, singleton_add]
  have C :
    Tendsto (fun r : ℝ => μ (s ∩ ({ x } + r • t)) / μ (closedBall x r) * (μ (closedBall x r) / μ ({ x } + r • u)))
      (𝓝[>] 0) (𝓝 (0 * (μ (closedBall x 1) / μ ({ x } + u)))) :=
    by
    apply ENNReal.Tendsto.mul A _ B (Or.inr ENNReal.zero_ne_top)
    simp [ENNReal.div_eq_top, h'u, measure_closedBall_lt_top.ne]
  simp only [zero_mul] at C
  apply C.congr' _
  filter_upwards [self_mem_nhdsWithin]
  rintro r (rpos : 0 < r)
  calc
    μ (s ∩ ({ x } + r • t)) / μ (closedBall x r) * (μ (closedBall x r) / μ ({ x } + r • u)) =
        μ (closedBall x r) * (μ (closedBall x r))⁻¹ * (μ (s ∩ ({ x } + r • t)) / μ ({ x } + r • u)) :=
      by simp only [div_eq_mul_inv]; ring
    _ = μ (s ∩ ({ x } + r • t)) / μ ({ x } + r • u) := by
      rw [ENNReal.mul_inv_cancel (measure_closedBall_pos μ x rpos).ne' measure_closedBall_lt_top.ne, one_mul]

Похожие утверждения