OAI/Analysis/AffineBernstein/TriangularGraph.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AffineBernstein.sourceEpigraph line 12

   Source documentation

   The manuscript's epigraph; the domain is not silently replaced by all of space.

   def sourceEpigraph {n : ℕ} (Ω : Set (Space n)) (u : Space n → ℝ) : Set (Space n × ℝ) :=
   …

   Mentions: OAI.AffineBernstein.Space

2. def OAI.AffineBernstein.triangularLinearHeight line 15
3. lemma OAI.AffineBernstein.triangularLinearHeight_apply line 20
4. def OAI.AffineBernstein.triangularGraphFunction line 24
5. lemma OAI.AffineBernstein.triangularGraphFunction_eval line 31
6. lemma OAI.AffineBernstein.triangularGraphFunction_image line 41
7. lemma OAI.AffineBernstein.triangularGraph_regular line 53
8. lemma OAI.AffineBernstein.triangular_sourceEpigraph_image line 73

   Source documentation

   The affine image is literally the epigraph of the derived graph; no new solution or geometric stationary surrogate is assumed.

   lemma triangular_sourceEpigraph_image {n : ℕ} (Ω : Set (Space n)) (u : Space n → ℝ)
       (M : (Space n × ℝ) ≃L[ℝ] (Space n × ℝ)) {c : ℝ}
       (hc : M (0,1) = (0,c)) (hcp : 0 < c) (v : Space n × ℝ) :
       (fun p => M p+v) '' sourceEpigraph Ω u =
         sourceEpigraph {y | (triangularBaseEquiv M hc hcp.ne').symm (y-v.1) ∈ Ω}
           (triangularGraphFunction u M hc hcp.ne' v) := by
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.sourceEpigraph, OAI.AffineBernstein.triangularBaseEquiv, OAI.AffineBernstein.triangularGraphFunction