English
Let t be a rational number. Then the infimum of the function r ↦ defaultRatCDF(r) over all rationals r with r > t equals default RatCDF at t, i.e. ⨅ r>Ioi t defaultRatCDF(r) = defaultRatCDF(t).
Русский
Пусть t — рациональное число. Тогда инфимум функции r ↦ defaultRatCDF(r) над всеми рациональными r, большими чем t, равен значению defaultRatCDF в t, то есть ⨅ r>t defaultRatCDF(r) = defaultRatCDF(t).
LaTeX
$$$$\\inf_{r > t} \\mathrm{defaultRatCDF}(r) = \\mathrm{defaultRatCDF}(t).$$$$
Lean4
theorem iInf_rat_gt_defaultRatCDF (t : ℚ) : ⨅ r : Ioi t, defaultRatCDF r = defaultRatCDF t :=
by
simp only [defaultRatCDF]
have h_bdd : BddBelow (range fun r : ↥(Ioi t) ↦ ite ((r : ℚ) < 0) (0 : ℝ) 1) :=
by
refine ⟨0, fun x hx ↦ ?_⟩
obtain ⟨y, rfl⟩ := mem_range.mpr hx
dsimp only
split_ifs
exacts [le_rfl, zero_le_one]
split_ifs with h
· refine le_antisymm ?_ (le_ciInf fun x ↦ ?_)
· obtain ⟨q, htq, hq_neg⟩ : ∃ q, t < q ∧ q < 0 := ⟨t / 2, by linarith, by linarith⟩
refine (ciInf_le h_bdd ⟨q, htq⟩).trans ?_
rw [if_pos]
rwa [Subtype.coe_mk]
· split_ifs
exacts [le_rfl, zero_le_one]
· refine le_antisymm ?_ ?_
· refine (ciInf_le h_bdd ⟨t + 1, lt_add_one t⟩).trans ?_
split_ifs
exacts [zero_le_one, le_rfl]
· refine le_ciInf fun x ↦ ?_
rw [if_neg]
rw [not_lt] at h ⊢
exact h.trans (mem_Ioi.mp x.prop).le
