John nirenberg iteration

theorem john_nirenberg_iteration    {B : Set E} {E_lam : ℝ → Set E}    (_hB : MeasurableSet B) (_hB_fin : volume B ≠ ⊤)    (hE_sub : ∀ lam, E_lam lam ⊆ B)    (_hE_meas : ∀ lam, MeasurableSet (E_lam lam))    (_hE_anti : ∀ lam₁ lam₂, lam₁ ≤ lam₂ → E_lam lam₂ ⊆ E_lam lam₁)    {A : ℝ} (hA : 0 < A)    {θ : ℝ} (hθ_pos : 0 < θ) (hθ_lt : θ < 1)    (h_decay : ∀ lam : ℝ, 0 < lam → volume (E_lam (lam + A)) ≤ ENNReal.ofReal θ * volume (E_lam lam)) :    ∀ lam : ℝ, 0 < lam →      volume (E_lam lam) ≤ ENNReal.ofReal (1 / θ) * volume B *        ENNReal.ofReal (Real.exp (-lam * (-Real.log θ / A))) := by  intro lam hlam  have hlamA_pos : 0 < lam / A := div_pos hlam hA  have hceil_ge1 : 1 ≤ ⌈lam / A⌉₊ := Nat.ceil_pos.mpr hlamA_pos  set n := ⌈lam / A⌉₊ - 1 with hn_def  set lam₀ := lam - ↑n * A with hlam0_def  have hlam0_pos : 0 < lam₀ := by    have hn_lt : (↑n : ℝ) < lam / A := by      rw [hn_def, Nat.cast_sub hceil_ge1]      push_cast      linarith [Nat.ceil_lt_add_one (le_of_lt hlamA_pos)]    have := mul_lt_mul_of_pos_right hn_lt hA    rw [div_mul_cancel₀] at this    · linarith    · exact ne_of_gt hA  have hlam_eq : lam₀ + ↑n * A = lam := by    ring  have h_iter := john_nirenberg_iteration_decay_iterate hA h_decay lam₀ hlam0_pos n  rw [hlam_eq] at h_iter  have h_sub : volume (E_lam lam₀) ≤ volume B := measure_mono (hE_sub lam₀)  have hn_ge : (↑n : ℝ) ≥ lam / A - 1 := by    rw [hn_def, Nat.cast_sub hceil_ge1]    push_cast    linarith [Nat.le_ceil (lam / A)]  calc    volume (E_lam lam)        ≤ ENNReal.ofReal θ ^ n * volume (E_lam lam₀) := h_iter    _ ≤ ENNReal.ofReal θ ^ n * volume B := by        gcongr    _ = ENNReal.ofReal (θ ^ n) * volume B := by        rw [john_nirenberg_iteration_ofReal_pow θ (le_of_lt hθ_pos) n]    _ ≤ (ENNReal.ofReal (1 / θ) * ENNReal.ofReal (Real.exp (-lam * (-Real.log θ / A)))) * volume B := by        gcongr        exact john_nirenberg_iteration_rpow_bound θ lam A hθ_pos hθ_lt n hn_ge    _ = ENNReal.ofReal (1 / θ) * volume B * ENNReal.ofReal (Real.exp (-lam * (-Real.log θ / A))) := by        ring