John nirenberg

theorem john_nirenberg    {u : E → ℝ} {x₀ : E} {r t A θ : ℝ}    (_hr : 0 < r) (ht : 0 < t) (hu_meas : Measurable u)    (hA : 0 < A) (hθ_pos : 0 < θ) (hθ_lt : θ < 1)    (h_decay : ∀ lam : ℝ, 0 < 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})) :    volume ({x ∈ Metric.ball x₀ r |      ‖u x - ⨍ y in Metric.ball x₀ r, u y ∂volume‖ > t}) ≤    ENNReal.ofReal (1 / θ) * volume (Metric.ball x₀ r) *      ENNReal.ofReal (Real.exp (-t * (-Real.log θ / A))) := by  set avg := ⨍ y in Metric.ball x₀ r, u y ∂volume  set E_lam : ℝ → Set E := fun lam => {x ∈ Metric.ball x₀ r | ‖u x - avg‖ > lam}  have hball_meas : MeasurableSet (Metric.ball x₀ r) := measurableSet_ball  have hE_sub : ∀ lam, E_lam lam ⊆ Metric.ball x₀ r := fun lam x hx => hx.1  have hE_meas : ∀ lam, MeasurableSet (E_lam lam) := by    intro lam    exact hball_meas.inter (measurableSet_lt measurable_const ((hu_meas.sub_const avg).norm))  have hE_anti : ∀ lam₁ lam₂, lam₁ ≤ lam₂ → E_lam lam₂ ⊆ E_lam lam₁ := by    intro lam₁ lam₂ hle x hx    exact ⟨hx.1, lt_of_le_of_lt hle hx.2⟩  simpa [E_lam, avg] using    john_nirenberg_iteration hball_meas (measure_ball_lt_top (μ := volume) (x := x₀) (r := r)).ne      hE_sub hE_meas hE_anti hA hθ_pos hθ_lt h_decay t ht