Harnack

theorem harnack    (hd : 2 < (d : ℝ))    (A : NormalizedEllipticCoeff d (Metric.ball (0 : E) 1))    {u : E → ℝ}    (hu_pos : ∀ x ∈ Metric.ball (0 : E) 1, 0 < u x)    (hsol : IsSolution A.1 u) :    essSup u μhalf ≤      Real.exp (C_harnack d * A.1.Λ ^ ((1 : ℝ) / 2)) *        essInf u μhalf := by  let K : ℝ := localHarnackConstant (d := d) A  have hK_pos : 0 < K := localHarnackConstant_pos (d := d) hd A  let centerOf : E → E := fun x => (15 / 16 : ℝ) • x  have hcenter_mem :      ∀ x ∈ Metric.closedBall (0 : E) (1 / 2 : ℝ),        centerOf x ∈ Metric.ball (0 : E) (1 / 2 : ℝ) := by    intro x hx    rw [Metric.mem_ball, dist_eq_norm, sub_zero]    have hxnorm : ‖x‖ ≤ 1 / 2 := by simpa [dist_eq_norm] using hx    dsimp [centerOf]    rw [norm_smul, Real.norm_of_nonneg (by positivity)]    calc      (15 / 16 : ℝ) * ‖x‖ ≤ (15 / 16 : ℝ) * (1 / 2 : ℝ) := by gcongr      _ = 15 / 32 := by norm_num      _ < 1 / 2 := by norm_num  have hmem_cover_ball :      ∀ x ∈ Metric.closedBall (0 : E) (1 / 2 : ℝ),        x ∈ Metric.ball (centerOf x) (1 / 16 : ℝ) := by    intro x hx    rw [Metric.mem_ball, dist_eq_norm]    have hxnorm : ‖x‖ ≤ 1 / 2 := by simpa [dist_eq_norm] using hx    have hrepr : x - centerOf x = (1 / 16 : ℝ) • x := by      dsimp [centerOf]      calc        x - (15 / 16 : ℝ) • x = (1 : ℝ) • x - (15 / 16 : ℝ) • x := by simp        _ = ((1 : ℝ) - 15 / 16) • x := by rw [sub_smul]        _ = (1 / 16 : ℝ) • x := by norm_num    rw [hrepr, norm_smul, Real.norm_of_nonneg (by positivity)]    calc      (1 / 16 : ℝ) * ‖x‖ ≤ (1 / 16 : ℝ) * (1 / 2 : ℝ) := by gcongr      _ = 1 / 32 := by norm_num      _ < 1 / 16 := by norm_num  obtain ⟨t, ht_mem, hcover⟩ :=    (isCompact_closedBall (0 : E) (1 / 2 : ℝ)).elim_nhds_subcover      (fun x : E => Metric.ball (centerOf x) (1 / 16 : ℝ))      (fun x hx => IsOpen.mem_nhds Metric.isOpen_ball (hmem_cover_ball x hx))  have hzero_mem : (0 : E) ∈ Metric.ball (0 : E) (1 / 2 : ℝ) := by    exact Metric.mem_ball_self (by norm_num)  have hsubset_cover :      Metric.ball (0 : E) (1 / 2 : ℝ) ⊆ ⋃ x ∈ t, Metric.ball (centerOf x) (1 / 16 : ℝ) := by    exact Metric.ball_subset_closedBall.trans hcover  have hnonneg_half_ae : ∀ᵐ x ∂ μhalf, 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 / 2 : ℝ) ≤ 1) hx)).le  have hnonneg_on_eighthBall :      ∀ {c z : E},        c ∈ Metric.ball (0 : E) (1 / 2 : ℝ) →        z ∈ Metric.ball c (1 / 8 : ℝ) →        0 ≤ u z := by    intro c z hc hz    have hc_closed : c ∈ Metric.closedBall (0 : E) (1 / 2 : ℝ) := by      exact Metric.mem_closedBall.2 (le_of_lt (Metric.mem_ball.1 hc))    have hz_unit : z ∈ Metric.ball (0 : E) 1 :=      ball_subset_unitBall_of_mem_closedBall_half (d := d) hc_closed (by positivity) (by norm_num) hz    exact (hu_pos z hz_unit).le  have hupper0 :      ∀ᵐ x ∂ μhalf, u x ≤ K ^ 17 * quarterBallInf u 0 := by    refine ae_on_set_of_ae_on_finite_cover (μ := volume)      (s := Metric.ball (0 : E) (1 / 2 : ℝ))      (U := fun x : E => Metric.ball (centerOf x) (1 / 16 : ℝ))      hsubset_cover ?_    intro x hx    let c : E := centerOf x    have hc_ball : c ∈ Metric.ball (0 : E) (1 / 2 : ℝ) := hcenter_mem x (ht_mem x hx)    have hchain :        quarterBallInf u c ≤ K ^ 16 * quarterBallInf u 0 := by      simpa [K] using        quarterBallInf_chain_le (d := d) hd A hu_pos hsol hc_ball hzero_mem    filter_upwards [ae_le_localHarnack_on_eighthBall (d := d) hd A hu_pos hsol hc_ball] with x hx    calc      u x ≤ K * quarterBallInf u c := by simpa [K] using hx      _ ≤ K * (K ^ 16 * quarterBallInf u 0) := by            gcongr      _ = K ^ 17 * quarterBallInf u 0 := by            rw [pow_succ']            ring  have hcore :      essSup u μhalf ≤ K ^ 17 * essInf u μhalf := by    have hcenter_bound :        ∀ {y : E}, y ∈ Metric.ball (0 : E) (1 / 2 : ℝ) →          essSup u μhalf ≤ K ^ 17 * quarterBallInf u y := by      intro y hy      have hhalf :          ∀ᵐ x ∂ μhalf, u x ≤ K ^ 17 * quarterBallInf u y := by        refine ae_on_set_of_ae_on_finite_cover (μ := volume)          (s := Metric.ball (0 : E) (1 / 2 : ℝ))          (U := fun x : E => Metric.ball (centerOf x) (1 / 16 : ℝ))          hsubset_cover ?_        intro x hx        let c : E := centerOf x        have hc_ball : c ∈ Metric.ball (0 : E) (1 / 2 : ℝ) := hcenter_mem x (ht_mem x hx)        have hchain :            quarterBallInf u c ≤ K ^ 16 * quarterBallInf u y := by          simpa [K] using            quarterBallInf_chain_le (d := d) hd A hu_pos hsol hc_ball hy        filter_upwards [ae_le_localHarnack_on_eighthBall (d := d) hd A hu_pos hsol hc_ball] with x hx        calc          u x ≤ K * quarterBallInf u c := by simpa [K] using hx          _ ≤ K * (K ^ 16 * quarterBallInf u y) := by                gcongr          _ = K ^ 17 * quarterBallInf u y := by                rw [pow_succ']                ring      exact essSup_halfBall_le_of_ae_bound hnonneg_half_ae hhalf    have hlow_ae :        ∀ᵐ y ∂ μhalf, essSup u μhalf / K ^ 17 ≤ u y := by      refine ae_on_set_of_ae_on_finite_cover (μ := volume)        (s := Metric.ball (0 : E) (1 / 2 : ℝ))        (U := fun x : E => Metric.ball (centerOf x) (1 / 16 : ℝ))        hsubset_cover ?_      intro x hx      let c : E := centerOf x      have hc_ball : c ∈ Metric.ball (0 : E) (1 / 2 : ℝ) := hcenter_mem x (ht_mem x hx)      have hcenter_div :          essSup u μhalf / K ^ 17 ≤ quarterBallInf u c := by        exact (div_le_iff₀ (pow_pos hK_pos 17)).2          (by simpa [mul_comm, mul_left_comm, mul_assoc] using hcenter_bound hc_ball)      have hu_ae_c :          AEMeasurable u (volume.restrict (Metric.ball c (1 / 8 : ℝ))) := by        have hsub_c : Metric.ball c (1 / 8 : ℝ) ⊆ Metric.ball (0 : E) 1 := by          intro z hz          have hc_closed : c ∈ Metric.closedBall (0 : E) (1 / 2 : ℝ) := by            exact Metric.mem_closedBall.2 (le_of_lt (Metric.mem_ball.1 hc_ball))          exact ball_subset_unitBall_of_mem_closedBall_half            (d := d) hc_closed (by positivity) (by norm_num) hz        exact aemeasurable_on_ball_of_isSolution (d := d) A hsol hsub_c      have hquarter_small :          ∀ᵐ z ∂ volume.restrict (Metric.ball c (1 / 16 : ℝ)),            quarterBallInf u c ≤ u z := by        refine ae_restrict_of_ae_restrict_of_subset          (Metric.ball_subset_ball (by norm_num : (1 / 16 : ℝ) ≤ 1 / 8)) ?_        exact quarterBallInf_le_ae (c := c) hu_ae_c (fun z hz => hnonneg_on_eighthBall hc_ball hz)      filter_upwards [hquarter_small] with z hz      exact le_trans hcenter_div hz    have hlow :        essSup u μhalf / K ^ 17 ≤ essInf u μhalf :=      le_essInf_halfBall_of_ae_bound hlow_ae hupper0    have hmul : essSup u μhalf ≤ essInf u μhalf * K ^ 17 :=      (div_le_iff₀ (pow_pos hK_pos 17)).mp hlow    simpa [mul_comm, mul_left_comm, mul_assoc, K] using hmul  have hessInf_nonneg : 0 ≤ essInf u μhalf := by    exact      le_essInf_real_of_ae_le        (μ := μhalf)        (restrict_ball_ne_zero (c := (0 : E)) (r := (1 / 2 : ℝ)) (by norm_num))        (by simpa using hnonneg_half_ae)  have hKexp :      K ^ 17 ≤ Real.exp (C_harnack d * A.1.Λ ^ ((1 : ℝ) / 2)) := by    simpa [K] using localHarnackConstant_pow_seventeen_le_exp (d := d) hd A  calc    essSup u μhalf ≤ K ^ 17 * essInf u μhalf := hcore    _ ≤ Real.exp (C_harnack d * A.1.Λ ^ ((1 : ℝ) / 2)) * essInf u μhalf := by          exact mul_le_mul_of_nonneg_right hKexp hessInf_nonneg