Documentation

LeanPool.Rado.Surface.Barriers

The two-disk configuration and its barriers #

Step 5 of Rado/PLAN.md: the fixed configuration in a chart whose target contains ball 0 8 — remove the preimages of the closed unit disks at ±4 (configY), take the Perron family with boundary condition ≤ 0 on the disk at -4 (configFamily), and force nonconstancy of its upper envelope with two explicit log-barriers on the annuli 1 ≤ |ζ ∓ 4| ≤ 2: values ≥ 3/4 resp. ≤ 1/4 at the witness points ±4 + 2^(1/4).

The two-disk configuration and its barriers #

Fixed configuration in a chart e whose target contains ball 0 8: the removed disks are the preimages of the closed unit disks at ±4, the barriers live on the annuli 1 ≤ |ζ ∓ 4| ≤ 2 (Rado/Complex/PlanarConnected.lean).

source
def Rado.configY {X : Type u_1} [TopologicalSpace X] (e : OpenPartialHomeomorph X ℂ) :
Set X

The surface X minus the two closed configuration disks.

Equations
Instances For
    source
    def Rado.configFamily {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (e : OpenPartialHomeomorph X ℂ) :
    Set (X → ℝ)

    The Perron family for the configuration: subharmonic on configY, [0,1]-valued there, continuous up to the closure, and ≤ 0 on the boundary circle of the disk at -4.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Rado.closedBall_config_subset {c : ℂ} (hc : ‖c‖ = 4) {r : ℝ} (hr : r ≤ 2) :
      Metric.closedBall c r ⊆ Metric.ball 0 8

      Both configuration disks (in fact, both surrounding annuli) lie inside the standard ball.

      source
      theorem Rado.isOpen_configY {X : Type u_1} [TopologicalSpace X] {e : OpenPartialHomeomorph X ℂ} (hb : Metric.ball 0 8 ⊆ e.target) [T2Space X] :
      IsOpen (configY e)

      configY is open.

      source
      theorem Rado.witness_mem_configY {X : Type u_1} [TopologicalSpace X] {e : OpenPartialHomeomorph X ℂ} (hb : Metric.ball 0 8 ⊆ e.target) :
      ↑e.symm (4 + 2 ^ (1 / 4)) ∈ configY e ∧ ↑e.symm (-4 + 2 ^ (1 / 4)) ∈ configY e

      Both witness points lie in configY.

      source
      theorem Rado.isConnected_configY {X : Type u_1} [TopologicalSpace X] {e : OpenPartialHomeomorph X ℂ} (hb : Metric.ball 0 8 ⊆ e.target) [ConnectedSpace X] [T2Space X] :
      IsConnected (configY e)

      configY is connected when X is (clopen argument through the chart, using isPathConnected_ball_diff_two_disks).

      source
      theorem Rado.isPerronFamily_configFamily {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {e : OpenPartialHomeomorph X ℂ} (hb : Metric.ball 0 8 ⊆ e.target) [T2Space X] :
      IsPerronFamily (configFamily e) (configY e)

      The configuration family is a Perron family.

      source
      theorem Rado.perronSup_ge_witness {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] {e : OpenPartialHomeomorph X ℂ} (he : e ∈ riemannAtlas X) (hb : Metric.ball 0 8 ⊆ e.target) [T2Space X] :
      3 / 4 ≤ perronSup (configFamily e) (↑e.symm (4 + 2 ^ (1 / 4)))

      The lower barrier: forced value ≥ 3/4 at the witness point near the disk at +4 (the function max 0 (log(2/|ζ-4|)/log 2) belongs to the family).

      source
      theorem Rado.perronSup_le_witness {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {e : OpenPartialHomeomorph X ℂ} (he : e ∈ riemannAtlas X) (hb : Metric.ball 0 8 ⊆ e.target) [T2Space X] :
      perronSup (configFamily e) (↑e.symm (-4 + 2 ^ (1 / 4))) ≤ 1 / 4

      The upper barrier: forced value ≤ 1/4 at the witness point near the disk at -4 (every family member is dominated on the annulus by 1 - log(2/|ζ+4|)/log 2, by the boundary comparison principle).