AffineInvariantCap.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.AffineBernstein.affineGraphConormal line 15
Source documentation
The inward conormal of the actual affine-image graph, pulled back to its original base. Its norm is NOT replaced by a vertical component.
```
def affineGraphConormal {n : ℕ} (u : Space n → ℝ)
    (L : (Space n × ℝ) ≃L[ℝ] (Space n × ℝ)) (x : Space n) :
    (Space n × ℝ) →L[ℝ] ℝ :=
…
```
Mentions: OAI.AffineBernstein.Space
lemma OAI.AffineBernstein.affineGraphConormal_apply line 21
lemma OAI.AffineBernstein.continuousAt_affineGraphConormal line 25
lemma OAI.AffineBernstein.affine_epigraph_support line 32

lemma OAI.AffineBernstein.affine_inner_ball_radialSupport line 47

Source documentation

The actual inner ball produces the conormal-normalized radial support bound required in the cap estimate. It is uniform under arbitrary affine maps.

lemma affine_inner_ball_radialSupport {n : ℕ} {Ω : Set (Space n)} {u : Space n → ℝ}
    (hc : ConvexOn ℝ Ω u) {x : Space n} (hx : x ∈ Ω) (hd : DifferentiableAt ℝ u x)
    (L : (Space n × ℝ) ≃L[ℝ] (Space n × ℝ)) (v : Space n × ℝ)
    (o : Space n) (c : ℝ) {r : ℝ} (hr : 0 < r)
    (hb : Metric.closedBall (L (o,c)+v) r ⊆ (fun p => L p+v) '' sourceEpigraph Ω u) :
    r*‖affineGraphConormal u L x‖ ≤ radialSupport u o c x := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.sourceEpigraph, OAI.AffineBernstein.affineGraphConormal, OAI.AffineBernstein.radialSupport

theorem OAI.AffineBernstein.affineMaximal_uniform_affine_cap_bound line 66

Source documentation

Uniform affine-image cap estimate, derived from the original PDE. The scalar is the inverse second-form norm with the actual inward unit conormal. The determinant on the left is the genuine affine-area covariance. No transformed-PDE premise or conormal bound is assumed.

theorem affineMaximal_uniform_affine_cap_bound (n : ℕ)
    {ε r R : ℝ} (hε : 0 < ε) (hr : 0 < r) (hR : 0 ≤ R)
    (t₀ t₁ q₀ : ℝ) :
    ∃ C > 0, ∀ {Ω : Set (Space n)}, IsOpen Ω → Convex ℝ Ω →
      ∀ {u : Space n → ℝ}, ContDiffOn ℝ ∞ u Ω →
      (∀ x ∈ Ω, (hessian u x).PosDef) → AffineMaximalOn Ω u →
      ∀ (L : (Space n × ℝ) ≃L[ℝ] (Space n × ℝ)) (v : Space n × ℝ)
        (o : Space n) (c : ℝ) (a : Space n →L[ℝ] ℝ) (b d : ℝ),
      Metric.closedBall (L (o,c)+v) r ⊆ (fun p => L p+v) '' sourceEpigraph Ω u →
      a o+b*c+d = q₀ →
      ∀ {K Q : Set (Space n)}, IsCompact K → K ⊆ Ω → MeasurableSet Q → Q ⊆ K →
      (∀ x ∈ Ω, x ∉ K → t₁+ε ≤ graphAffineFunction u a b d x) →
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.AffineMaximalOn, OAI.AffineBernstein.sourceEpigraph, OAI.AffineBernstein.graphAffineFunction