Measure Real exists abs lt le

lemma measureReal_exists_abs_lt_le [OrderBot ι] [IsFiniteMeasure μ]    (hX : StronglyAdapted 𝓕 X) (hXint : ∀ s, Integrable (X s) μ) {C : ℝ}    (hC : ∀ S : ElementaryPredictableSet 𝓕, μ[(S.indicator (1 : ℝ) ● X) t] ≤ C)    (hlam : 0 < lam) (hF : ∀ s ∈ F, s ≤ t) :    μ.real {ω | ∃ s ∈ F, lam < |X s ω|}      ≤ 2 * (C + ∫ ω, |X t ω - X ⊥ ω| ∂μ + ∫ ω, |X ⊥ ω| ∂μ + ∫ ω, |X t ω| ∂μ) / lam := by  set G : Finset ι := insert ⊥ F with hG  have hGF : F ⊆ G := subset_insert _ _  have hGle : ∀ s ∈ G, s ≤ t := by simp [G]; grind  set n : ℕ := G.card with hn  set idx : ℕ → ι := finIdx G t with hidx  have hmono : Monotone idx := finIdx_monotone hGle  have hidx0 : idx 0 = ⊥ := finIdx_zero_eq_bot (mem_insert_self _ _)  have hidxn : idx n = t := finIdx_eq_of_card_le hn.ge  -- two-sided expectation bound for adapted 0/1 weights along `idx`  have hbdd : ∀ W : ℕ → Ω → ℝ, (∀ k, k < n → ∀ ω, W k ω = 0 ∨ W k ω = 1) →      (∀ k, k < n → Measurable[𝓕 (idx k)] (W k)) →      ∫ ω, (∑ k ∈ range n, W k ω * (X (idx (k + 1)) ω - X (idx k) ω)) ∂μ        ∈ Set.Icc (-(C + ∫ ω, |X (idx n) ω - X (idx 0) ω| ∂μ)) C :=    fun W hW01 hWmeas ↦ integral_sum_weight_increments_mem_Icc (t := t) hXint hC hmono      (finIdx_le hGle) hW01 hWmeas  -- apply the one-sided maximal inequality to `X`  have hpos := mul_measureReal_exists_lt_le (lam := lam) hX hXint (n := n) hmono (K := C)    (fun W hW01 hWmeas ↦ (hbdd W hW01 hWmeas).2)  -- and to `-X`  have hnegX : StronglyAdapted 𝓕 (fun s ω ↦ -X s ω) := fun s ↦ (hX s).neg  have hnegint : ∀ s, Integrable ((fun s ω ↦ -X s ω) s) μ := fun s ↦ (hXint s).neg  have hneg := mul_measureReal_exists_lt_le (lam := lam) hnegX hnegint (n := n) hmono    (K := C + ∫ ω, |X (idx n) ω - X (idx 0) ω| ∂μ)    (fun W hW01 hWmeas ↦ by      have h1 := (hbdd W hW01 hWmeas).1      have h2 : ∫ ω, (∑ k ∈ range n, W k ω * (-X (idx (k + 1)) ω - -X (idx k) ω)) ∂μ          = -∫ ω, (∑ k ∈ range n, W k ω * (X (idx (k + 1)) ω - X (idx k) ω)) ∂μ := by        rw [← integral_neg]        congr 1 with ω        rw [← sum_neg_distrib]        grind      rw [h2]      linarith)  -- combine the two events  have hsub : {ω | ∃ s ∈ F, lam < |X s ω|}      ⊆ {ω | ∃ k ≤ n, lam < X (idx k) ω} ∪ {ω | ∃ k ≤ n, lam < -X (idx k) ω} := by    rintro ω ⟨s, hs, habs⟩    obtain ⟨k, hk, hkeq⟩ := exists_finIdx_eq (t := t) (hGF hs)    grind  have habs u : ∫ ω, |(fun s ω ↦ -X s ω) u ω| ∂μ = ∫ ω, |X u ω| ∂μ := by simp  rw [hidx0, hidxn] at hpos hneg  rw [habs ⊥, habs t] at hneg  have hunion : μ.real {ω | ∃ s ∈ F, lam < |X s ω|}      ≤ μ.real {ω | ∃ k ≤ n, lam < X (idx k) ω} + μ.real {ω | ∃ k ≤ n, lam < -X (idx k) ω} :=    (measureReal_mono hsub).trans (measureReal_union_le _ _)  have hI : (0 : ℝ) ≤ ∫ ω, |X t ω - X ⊥ ω| ∂μ := integral_nonneg fun ω ↦ abs_nonneg _  rw [le_div_iff₀ hlam]  have hmul : lam * μ.real {ω | ∃ s ∈ F, lam < |X s ω|}      ≤ lam * (μ.real {ω | ∃ k ≤ n, lam < X (idx k) ω}        + μ.real {ω | ∃ k ≤ n, lam < -X (idx k) ω}) :=    mul_le_mul_of_nonneg_left hunion hlam.le  rw [mul_add] at hmul  nlinarith [hpos, hneg, hmul]