Weak harnack

theorem weak_harnack    (hd : 2 < (d : ℝ))    (A : NormalizedEllipticCoeff d (ball (0 : E) 1))    {u : E → ℝ} {q : ℝ} (hq : 0 < q) (hq1 : q < 1)    (hu_pos : ∀ x ∈ ball (0 : E) 1, 0 < u x)    (hsuper : IsSupersolution A.1 u) :    (∫ x in ball (0 : E) (1 / 4 : ℝ),        |u x| ^ (q * (d : ℝ) / ((d : ℝ) - 2)) ∂volume) ^          (((d : ℝ) - 2) / (q * (d : ℝ))) ≤      (C_weakHarnack d hd / (1 - q) ^ (weak_harnack_decay_exp d)) ^        (A.1.Λ ^ ((1 : ℝ) / 2)) *        essInf u (volume.restrict (ball (0 : E) (1 / 4 : ℝ))) := by  set p₀ := weakHarnackP0 A with hp₀_def  have hp₀_pos : 0 < p₀ := p₀_pos A  have hinv_p₀ : 1 / p₀ = A.1.Λ ^ ((1 : ℝ) / 2) / c_crossover' d := by    rw [hp₀_def, weakHarnackP0]; field_simp  -- The chain at the p₀ level, using C_chain (un-powered constant).  have hchain := weak_harnack_chain hd A hq hq1 hu_pos hsuper  -- Abbreviations.  set I := ∫ x in ball (0 : E) (1 / 4 : ℝ),      |u x| ^ (q * (d : ℝ) / ((d : ℝ) - 2)) ∂volume  set α := p₀ * (((d : ℝ) - 2) / (q * (d : ℝ)))  set inf_u := essInf u (volume.restrict (ball (0 : E) (1 / 4 : ℝ)))  -- hchain: I^α ≤ (C_chain/(1-q)^d) · inf_u^{p₀}  -- Raise to 1/p₀: I^{α/p₀} ≤ (C_chain/(1-q)^d)^{1/p₀} · inf_u  have hI_nonneg : 0 ≤ I := integral_nonneg fun x => by positivity  have hC_nonneg : 0 ≤ C_chain (d := d) hd / (1 - q) ^ ((d : ℝ) * moserChi d) := by    exact div_nonneg (le_trans (by norm_num) (one_le_C_chain (d := d) hd))      (Real.rpow_nonneg (by linarith) _)  have hinf_nonneg : 0 ≤ inf_u := by    have hμ_ne_zero :        volume.restrict (ball (0 : E) (1 / 4 : ℝ)) ≠ 0 := by      intro hzero      have hball_zero : volume (ball (0 : E) (1 / 4 : ℝ)) = 0 := by        simpa [Measure.restrict_apply_univ] using          congrArg (fun μ : Measure E => μ Set.univ) hzero      exact (Metric.measure_ball_pos volume (0 : E) (by norm_num : 0 < (1 / 4 : ℝ))).ne'        hball_zero    have hquarter_nonneg :        ∀ᵐ x ∂(volume.restrict (ball (0 : E) (1 / 4 : ℝ))), (0 : ℝ) ≤ u x := by      filter_upwards [ae_restrict_mem measurableSet_ball] with x hx      exact (hu_pos x ((Metric.ball_subset_ball (by norm_num : (1 / 4 : ℝ) ≤ 1)) hx)).le    exact le_essInf_real_of_ae_le (d := d) hμ_ne_zero hquarter_nonneg  have hα_nonneg : 0 ≤ α := mul_nonneg hp₀_pos.le (div_nonneg (by linarith) (by positivity))  have hstep := rpow_le_rpow_of_exponent hI_nonneg hC_nonneg hinf_nonneg hp₀_pos hα_nonneg hchain  -- hstep: I^{α/p₀} ≤ (C_chain/(1-q)^d)^{1/p₀} · inf_u  -- α/p₀ = (d-2)/(qd).  have hα_div : α / p₀ = ((d : ℝ) - 2) / (q * (d : ℝ)) := by    simp only [α]; field_simp  rw [hα_div] at hstep  -- Key identity: (C_chain/(1-q)^d)^{1/p₀} = (C_chain^{1/c'}/(1-q)^{d/c'})^{Λ^{1/2}}  -- Since C_weakHarnack = C_chain^{1/c'}, this is (C_wH/(1-q)^{d/c'})^{Λ^{1/2}}.  -- So hstep gives exactly the stated bound.  have hconst_eq :      (C_chain (d := d) hd / (1 - q) ^ ((d : ℝ) * moserChi d)) ^ (1 / p₀) =        (C_weakHarnack d hd / (1 - q) ^ (weak_harnack_decay_exp d)) ^          (A.1.Λ ^ ((1 : ℝ) / 2)) := by    -- 1/p₀ = Λ^{1/2}/c'. So LHS = (C_chain/(1-q)^d)^{Λ^{1/2}/c'}.    -- Distribute: = C_chain^{Λ^{1/2}/c'} · (1-q)^{-d·Λ^{1/2}/c'}.    -- C_chain^{Λ^{1/2}/c'} = (C_chain^{1/c'})^{Λ^{1/2}} = C_wH^{Λ^{1/2}}.    -- (1-q)^{-d·Λ^{1/2}/c'} = ((1-q)^{d/c'})^{-Λ^{1/2}}.    -- Combined: (C_wH · (1-q)^{-d/c'})^{Λ^{1/2}} = (C_wH/(1-q)^{d/c'})^{Λ^{1/2}}.    rw [hinv_p₀]    -- Goal: (C_chain d / (1 - q) ^ (d : ℝ)) ^ (A.1.Λ ^ ((1:ℝ)/2) / c_crossover' d) =    --       (C_weakHarnack d / (1 - q) ^ weak_harnack_decay_exp d) ^ (A.1.Λ ^ ((1:ℝ)/2))    have hc'_pos := c_crossover'_pos (d := d)    have hc'_ne : c_crossover' (d := d) ≠ 0 := ne_of_gt hc'_pos    have h1q_pos : 0 < 1 - q := by linarith    have h1q_nonneg : 0 ≤ 1 - q := h1q_pos.le    have hbase_nonneg : 0 ≤ C_chain (d := d) hd / (1 - q) ^ ((d : ℝ) * moserChi d) :=      div_nonneg (le_trans (by norm_num) (one_le_C_chain (d := d) hd)) (by positivity)    have hexp_rw : A.1.Λ ^ ((1:ℝ)/2) / c_crossover' d =        (1 / c_crossover' d) * A.1.Λ ^ ((1:ℝ)/2) := by      rw [div_eq_inv_mul]; congr 1; exact (one_div _).symm    rw [hexp_rw]    rw [Real.rpow_mul hbase_nonneg]    -- Goal: ((C_chain d / (1 - q) ^ (d : ℝ)) ^ (1 / c_crossover' d)) ^ (Λ^{1/2}) =    --       (C_weakHarnack d / (1 - q) ^ weak_harnack_decay_exp d) ^ (Λ^{1/2})    congr 1    -- Goal: (C_chain d / (1 - q) ^ (d : ℝ)) ^ (1 / c_crossover' d) =    --       C_weakHarnack d / (1 - q) ^ weak_harnack_decay_exp d    rw [Real.div_rpow (le_trans (by norm_num) (one_le_C_chain (d := d) hd))        (Real.rpow_nonneg h1q_nonneg _)]    -- Goal: C_chain d ^ (1/c') / ((1-q)^d)^{1/c'} = C_wH / (1-q)^{d/c'}    rw [← C_weakHarnack_eq_C_chain_rpow (d := d) hd]    have : ((1 - q) ^ ((d : ℝ) * moserChi d)) ^ (1 / c_crossover' d) =        (1 - q) ^ weak_harnack_decay_exp d := by      rw [← Real.rpow_mul h1q_nonneg]      unfold weak_harnack_decay_exp      congr 1      rw [mul_one_div]    rw [this]  rw [hconst_eq] at hstep  exact hstep