John nirenberg from base

theorem john_nirenberg_from_base    {u : E → ℝ} {x₀ : E} {r : ℝ} {A θ : ℝ}    (_hr : 0 < r) (hu_meas : Measurable u)    (hA : 0 < A) (hθ_pos : 0 < θ) (hθ_lt : θ < 1)    (h_decay : ∀ lam : ℝ, A ≤ lam →      volume ({x ∈ Metric.ball x₀ r |        ‖u x - ⨍ y in Metric.ball x₀ r, u y ∂volume‖ > lam + A}) ≤        ENNReal.ofReal θ *          volume ({x ∈ Metric.ball x₀ r |            ‖u x - ⨍ y in Metric.ball x₀ r, u y ∂volume‖ > lam}))    (t : ℝ) (_ht : 0 < t) :    volume ({x ∈ Metric.ball x₀ r |      ‖u x - ⨍ y in Metric.ball x₀ r, u y ∂volume‖ > t}) ≤    ENNReal.ofReal (1 / θ ^ 2) * volume (Metric.ball x₀ r) *      ENNReal.ofReal (Real.exp (-t * (-Real.log θ / A))) := by  -- This is a purely mathematical iteration argument (no CZ covering involved).  -- The proof decomposes t into base + iterated steps, applies h_decay iteratively,  -- and bounds the resulting geometric series by the exponential.  set avg := ⨍ y in Metric.ball x₀ r, u y ∂volume  set B := Metric.ball x₀ r with hB_def  set F : ℝ → Set E := fun s => {x ∈ B | ‖u x - avg‖ > s + A} with hF_def  have hB_meas : MeasurableSet B := by    simpa [hB_def] using (measurableSet_ball : MeasurableSet (Metric.ball x₀ r))  have hF_sub : ∀ s, F s ⊆ B := by    intro s x hx    exact hx.1  have hF_meas : ∀ s, MeasurableSet (F s) := by    intro s    refine hB_meas.inter ?_    exact measurableSet_lt measurable_const ((hu_meas.sub_const avg).norm)  have hF_anti : ∀ s₁ s₂, s₁ ≤ s₂ → F s₂ ⊆ F s₁ := by    intro s₁ s₂ hs x hx    refine ⟨hx.1, ?_⟩    have hs' : s₁ + A ≤ s₂ + A := by linarith    exact lt_of_le_of_lt hs' hx.2  have h_decayF : ∀ s : ℝ, 0 < s →      volume (F (s + A)) ≤ ENNReal.ofReal θ * volume (F s) := by    intro s hs    have hsA : A ≤ s + A := by linarith    simpa [F, add_assoc, avg, B] using h_decay (s + A) hsA  have h_iter :=    john_nirenberg_iteration hB_meas      (measure_ball_lt_top (μ := volume) (x := x₀) (r := r)).ne      hF_sub hF_meas hF_anti hA hθ_pos hθ_lt h_decayF  have hAdiv : A * (-Real.log θ / A) = -Real.log θ := by    field_simp [hA.ne']  have hexpA : Real.exp (-A * (-Real.log θ / A)) = θ := by    have hexp_arg : -A * (-Real.log θ / A) = Real.log θ := by      calc        -A * (-Real.log θ / A) = -(A * (-Real.log θ / A)) := by ring        _ = -(-Real.log θ) := by rw [hAdiv]        _ = Real.log θ := by ring    rw [hexp_arg, Real.exp_log hθ_pos]  by_cases htA : A < t  · have hs_pos : 0 < t - A := by linarith    have hmain :        volume ({x ∈ Metric.ball x₀ r | ‖u x - avg‖ > t}) ≤          ENNReal.ofReal (1 / θ) * volume (Metric.ball x₀ r) *            ENNReal.ofReal (Real.exp (-(t - A) * (-Real.log θ / A))) := by      simpa [F, hB_def, avg, sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using        h_iter (t - A) hs_pos    have hexp_shift :        Real.exp (-(t - A) * (-Real.log θ / A)) =          (1 / θ) * Real.exp (-t * (-Real.log θ / A)) := by      have h_inv : (1 / θ : ℝ) = Real.exp (-Real.log θ) := by        rw [Real.exp_neg, Real.exp_log hθ_pos, one_div]      rw [h_inv, ← Real.exp_add]      congr 1      calc        -(t - A) * (-Real.log θ / A)            = -t * (-Real.log θ / A) + A * (-Real.log θ / A) := by ring        _ = -t * (-Real.log θ / A) + (-Real.log θ) := by rw [hAdiv]        _ = -Real.log θ + -t * (-Real.log θ / A) := by ring    calc      volume ({x ∈ Metric.ball x₀ r | ‖u x - avg‖ > t})          ≤ ENNReal.ofReal (1 / θ) * volume (Metric.ball x₀ r) *              ENNReal.ofReal (Real.exp (-(t - A) * (-Real.log θ / A))) := hmain      _ = ENNReal.ofReal (1 / θ ^ 2) * volume (Metric.ball x₀ r) *            ENNReal.ofReal (Real.exp (-t * (-Real.log θ / A))) := by        rw [hexp_shift, ENNReal.ofReal_mul (by positivity)]        calc          ENNReal.ofReal (1 / θ) * volume (Metric.ball x₀ r) *              (ENNReal.ofReal (1 / θ) * ENNReal.ofReal (Real.exp (-t * (-Real.log θ / A))))              =              (ENNReal.ofReal (1 / θ) * ENNReal.ofReal (1 / θ)) * volume (Metric.ball x₀ r) *                ENNReal.ofReal (Real.exp (-t * (-Real.log θ / A))) := by                ring          _ = ENNReal.ofReal ((1 / θ) * (1 / θ)) * volume (Metric.ball x₀ r) *                ENNReal.ofReal (Real.exp (-t * (-Real.log θ / A))) := by                rw [← ENNReal.ofReal_mul (by positivity)]          _ = ENNReal.ofReal (1 / θ ^ 2) * volume (Metric.ball x₀ r) *                ENNReal.ofReal (Real.exp (-t * (-Real.log θ / A))) := by                congr 1                field_simp [pow_two, hθ_pos.ne']  · have ht_le_A : t ≤ A := le_of_not_gt htA    have hsub :        {x ∈ Metric.ball x₀ r | ‖u x - avg‖ > t} ⊆ Metric.ball x₀ r := by      intro x hx      exact hx.1    have hrate_pos : 0 < -Real.log θ / A := by      have hlog_neg : Real.log θ < 0 := Real.log_neg hθ_pos hθ_lt      exact div_pos (by linarith) hA    have hexp_lower : θ ≤ Real.exp (-t * (-Real.log θ / A)) := by      have hArg : -A * (-Real.log θ / A) ≤ -t * (-Real.log θ / A) := by        nlinarith [ht_le_A, le_of_lt hrate_pos]      calc        θ = Real.exp (-A * (-Real.log θ / A)) := by rw [hexpA]        _ ≤ Real.exp (-t * (-Real.log θ / A)) := Real.exp_le_exp.2 hArg    have hmul : 1 ≤ (1 / θ ^ 2) * θ := by      have hθ_ne : θ ≠ 0 := hθ_pos.ne'      rw [pow_two]      field_simp [hθ_ne]      linarith    have hcoeff : 1 ≤ (1 / θ ^ 2) * Real.exp (-t * (-Real.log θ / A)) := by      calc        1 ≤ (1 / θ ^ 2) * θ := hmul        _ ≤ (1 / θ ^ 2) * Real.exp (-t * (-Real.log θ / A)) := by            gcongr    calc      volume ({x ∈ Metric.ball x₀ r | ‖u x - avg‖ > t})          ≤ volume (Metric.ball x₀ r) := measure_mono hsub      _ = ENNReal.ofReal 1 * volume (Metric.ball x₀ r) := by simp      _ ≤ ENNReal.ofReal ((1 / θ ^ 2) * Real.exp (-t * (-Real.log θ / A))) *            volume (Metric.ball x₀ r) := by            have hcoeff' :                ENNReal.ofReal (1 : ℝ) ≤                  ENNReal.ofReal ((1 / θ ^ 2) * Real.exp (-t * (-Real.log θ / A))) :=              ENNReal.ofReal_le_ofReal hcoeff            exact mul_le_mul_of_nonneg_right hcoeff' (by positivity)      _ = ENNReal.ofReal (1 / θ ^ 2) * volume (Metric.ball x₀ r) *            ENNReal.ofReal (Real.exp (-t * (-Real.log θ / A))) := by            rw [ENNReal.ofReal_mul (by positivity)]            ring