TargetCapLIntegral.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.AffineBernstein.targetGraphConormal line 14
Source documentation
The actual graph conormal expressed in an arbitrary fixed target space.
```
def targetGraphConormal {n : ℕ} (u : Space n → ℝ)
    (L : G ≃L[ℝ] (Space n × ℝ)) (x : Space n) : G →L[ℝ] ℝ :=
…
```
Mentions: OAI.AffineBernstein.Space
lemma OAI.AffineBernstein.targetGraphConormal_norm_le line 19

theorem OAI.AffineBernstein.affineMaximal_uniform_target_cap_lintegral_bound line 37

Source documentation

The uniform cap producer in a fixed normed target. Choosing target coordinates costs only constants depending on those fixed coordinates, never on the varying affine map. The nonnegative integral is the exact original inverse second form with actual conormal norm.

theorem affineMaximal_uniform_target_cap_lintegral_bound (n : ℕ)
    (T : G ≃L[ℝ] (Space 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 : G ≃L[ℝ] (Space n × ℝ)) (v : Space n × ℝ)
        (o : Space n) (c : ℝ) (a : Space n →L[ℝ] ℝ) (b d : ℝ),
      Metric.closedBall (L.symm ((o,c)-v)) r ⊆
        (fun p => L.symm (p-v)) '' sourceEpigraph Ω u →
      a o+b*c+d = q₀ →
…

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