English
A technical identity for measures: ⨅ r with t<r of ρ(s×Iic r) equals ρ(s×Iic t).
Русский
Техническая идентичность для меры: инфimum по r с t<r от ρ(s×Iic r) равно ρ(s×Iic t).
LaTeX
$$$\iinf_{r:\; t< r} ρ(s × I_i c r) = ρ(s × I_i c t).$$$
Lean4
theorem _root_.MeasureTheory.Measure.iInf_rat_gt_prod_Iic {ρ : Measure (α × ℝ)} [IsFiniteMeasure ρ] {s : Set α}
(hs : MeasurableSet s) (t : ℚ) : ⨅ r : { r' : ℚ // t < r' }, ρ (s ×ˢ Iic (r : ℝ)) = ρ (s ×ˢ Iic (t : ℝ)) :=
by
rw [← Monotone.measure_iInter]
· rw [← prod_iInter]
congr with x : 1
simp only [mem_iInter, mem_Iic, Subtype.forall]
refine ⟨fun h ↦ ?_, fun h a hta ↦ h.trans ?_⟩
· refine le_of_forall_lt_rat_imp_le fun q htq ↦ h q ?_
exact mod_cast htq
· exact mod_cast hta.le
· exact fun r r' hrr' ↦ prod_mono_right <| by gcongr
· exact fun _ => (hs.prod measurableSet_Iic).nullMeasurableSet
· exact ⟨⟨t + 1, lt_add_one _⟩, measure_ne_top ρ _⟩
