BoundedHarmonic.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.AffineBernstein.inverseHessianTrace_constant line 19

theorem OAI.AffineBernstein.normalized_harmonic_no_two_extremes line 25

Source documentation

A quantitative oscillation reduction on an actual normalized section. This is proved from the ABP low-set and logarithmic energy estimates above.

theorem normalized_harmonic_no_two_extremes {n : ℕ} (hn : 1 ≤ n) {ρ R : ℝ}
    (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (hR : 1 ≤ R) {d : ℝ} (hd : 0 < d) :
    ∃ ε : ℝ, 0 < ε ∧ ∀ v : Space n → ℝ, BalancedNormalized ρ R v →
      ∀ F : Space n → ℝ, ContDiff ℝ ∞ F → (∀ x, 0 ≤ F x ∧ F x ≤ d) →
      (∀ x, inverseHessianTrace v F x = 0) →
      ∀ a ∈ Metric.ball (0:Space n) (1/64:ℝ), ∀ b ∈ Metric.ball (0:Space n) (1/64:ℝ),
        ¬(F a ≤ ε ∧ d-F b ≤ ε) := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.BalancedNormalized, OAI.AffineBernstein.inverseHessianTrace

theorem OAI.AffineBernstein.centered_balanced_bounded_harmonic_constant line 101

Source documentation

Bounded harmonic Liouville for the genuine inverse-Hessian operator of an entire balanced affine-maximal graph. No CG/TW theorem is assumed.

theorem centered_balanced_bounded_harmonic_constant {n : ℕ} (hn : 1 ≤ n)
    {u F : Space n → ℝ} (hu : ContDiff ℝ ∞ u) (hp : ∀ x, (hessian u x).PosDef)
    (hm : AffineMaximalOn univ u) (hzero : u 0=0) (hdzero : fderiv ℝ u 0=0)
    {ρ : ℝ} (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (hbal : SectionBalance univ u ρ)
    (hF : ContDiff ℝ ∞ F) (hFb : BddBelow (range F)) (hFa : BddAbove (range F))
    (hLF : ∀ x, inverseHessianTrace u F x=0) : ∀ x y, F x=F y := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.AffineMaximalOn, OAI.AffineBernstein.SectionBalance, OAI.AffineBernstein.inverseHessianTrace