Harnack's inequality

Main Results

Theorem harnack_ineq:

A positive harmonic function u on the unit disc satisfies the inequalities (1 - ‖z‖) / (1 + ‖z‖) * u 0 ≤ u z ∧ u z ≤ u 0 * (1 + ‖z‖) / (1 - ‖z‖) for all z in the unit disc.

theorem LeanPool.LeanComplexAnalysis.non_neg_boundary (u : ℂ → ℝ) (t : ℝ) (h_pos : ∀ z ∈ Metric.ball 0 1, 0 < u z) (hc : ContinuousOn u (Metric.closedBall 0 1)) : 0 ≤ u (Complex.exp (↑t * Complex.I))

theorem LeanPool.LeanComplexAnalysis.harnack_ineq_cont_normalized_upper (u : ℂ → ℝ) (h_pos : ∀ z ∈ Metric.ball 0 1, 0 < u z) (h_f_zero : u 0 = 1) (h_harmonic : InnerProductSpace.HarmonicOnNhd u (Metric.ball 0 1)) (hc : ContinuousOn u (Metric.closedBall 0 1)) (z : ℂ) (hz : z ∈ Metric.ball 0 1) : u z ≤ (1 + ‖z‖) / (1 - ‖z‖)

theorem LeanPool.LeanComplexAnalysis.harnack_ineq_cont_normalized_lower (u : ℂ → ℝ) (h_pos : ∀ z ∈ Metric.ball 0 1, 0 < u z) (h_f_zero : u 0 = 1) (h_harmonic : InnerProductSpace.HarmonicOnNhd u (Metric.ball 0 1)) (hc : ContinuousOn u (Metric.closedBall 0 1)) (z : ℂ) (hz : z ∈ Metric.ball 0 1) : (1 - ‖z‖) / (1 + ‖z‖) ≤ u z

theorem LeanPool.LeanComplexAnalysis.harnack_ineq (u : ℂ → ℝ) (h_pos : ∀ z ∈ Metric.ball 0 1, 0 < u z) (h_harmonic : InnerProductSpace.HarmonicOnNhd u (Metric.ball 0 1)) (z : ℂ) (hz : z ∈ Metric.ball 0 1) : (1 - ‖z‖) / (1 + ‖z‖) * u 0 ≤ u z ∧ u z ≤ u 0 * (1 + ‖z‖) / (1 - ‖z‖)

Harnack's inequality for positive harmonic functions. A positive harmonic function on the unit disc satisfies two-sided estimates in terms of the distance to the boundary.