Q Relative Ent lower Semicontinuous

@[fun_prop]theorem qRelativeEnt.lowerSemicontinuous (ρ : MState d) : LowerSemicontinuous fun σ => 𝐃(ρ‖σ) := by  simp_rw [qRelativeEnt, SandwichedRelRentropy, if_true, lowerSemicontinuous_iff]  simp only [zero_lt_one, ↓reduceDIte]  intro x  by_cases hx : x.M.ker ≤ ρ.M.ker  · intro y hy    obtain ⟨y', hy'⟩ : ∃ y' : ℝ, y < ENNReal.ofReal y' ∧ y' < ⟪ρ.M, ρ.M.log - x.M.log⟫ := by      rcases ENNReal.lt_iff_exists_real_btwn.mp hy with ⟨ y', hy₁, hy₂ ⟩;      rw [ ENNReal.ofReal_lt_iff_lt_toReal ] at hy₂ <;> aesop;    simp only [↓reduceDIte, inner_sub_right, hx] at hy hy' ⊢    have := inner_log_bounded_near hx (y := ⟪ρ.M, ρ.M.log⟫ - y') (by linarith)    filter_upwards [this] with σ hσ    split    · simp_all only [ENNReal.ofReal, forall_const]      apply lt_of_lt_of_le hy'.1      refine mod_cast max_le (a := y') (b := 0) (c := ⟪ρ.M, ρ.M.log⟫ - ⟪ρ.M, σ.M.log⟫) ?_ ?_      · linarith      · linarith [ show 0 ≤ y' from le_of_not_gt fun h => by norm_num [ Real.toNNReal_of_nonpos h.le ] at hy' ]    · exact hy'.1.trans_le (by simp)  · intro y hy    simp only [hx, ↓reduceDIte] at hy ⊢    have h₂ := qRelativeEnt_lowerSemicontinuous_2 ρ x hx y hy    filter_upwards [h₂] with x' hx'    split_ifs with h₁ junk    · simpa [← EReal.coe_ennreal_lt_coe_ennreal_iff, h₁] using hx'    · simp at junk    · exact hy