UniformLogCells.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.AffineBernstein.logTubeMeasure_apply_le_cell line 16

Source documentation

A pushforward cell is bounded by any enclosing physical base cell. No integrability or finiteness assumption on the density is used.

lemma logTubeMeasure_apply_le_cell {k : ℕ} {E : Type*}
    [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
    [Nontrivial E] [MeasurableSpace E] [BorelSpace E]
    (μ : Measure (Space k)) [SFinite μ] (D : Set (Space k)) (F : Space k × E → ℝ)
    {K Q : Set (Space k)} (hK : MeasurableSet K)
    (hsub : D ∩ logSpace ⁻¹' K ⊆ Q) :
    logTubeMeasure μ D F K ≤
      ∫⁻ q : Space k × sphere (0:E) 1, ENNReal.ofReal (F (tubeLift q))
        ∂(μ.restrict Q).prod (volume : Measure E).toSphere := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.logSpace, OAI.AffineBernstein.logTubeMeasure, OAI.AffineBernstein.tubeLift

def OAI.AffineBernstein.logarithmicUnitCell line 35
Source documentation
Closed unit cells in the actual logarithmic base coordinates.
```
def logarithmicUnitCell (k : ℕ) (z : Fin k → ℤ) : Set (Space k) :=
…
```
Mentions: OAI.AffineBernstein.Space
lemma OAI.AffineBernstein.isClosed_logarithmicUnitCell line 38
lemma OAI.AffineBernstein.logarithmicUnitCell_preimage_subset line 48
Source documentation
A logarithmic unit cell fits in the physical factor-four cell about the exponential of its midpoint. The quantitative inclusion uses log(2)≥1/2.
```
lemma logarithmicUnitCell_preimage_subset {k : ℕ} (z : Fin k → ℤ) :
    positiveOrthant k ∩ logSpace ⁻¹' logarithmicUnitCell k z ⊆
      multiplicativeCell (expSpace (WithLp.toLp 2 (fun i => (z i:ℝ)+1/2))) := by
…
```
Mentions: OAI.AffineBernstein.positiveOrthant, OAI.AffineBernstein.logSpace, OAI.AffineBernstein.logarithmicUnitCell, OAI.AffineBernstein.multiplicativeCell, OAI.AffineBernstein.expSpace
lemma OAI.AffineBernstein.affineEpigraphLogMeasure_unitCell_le line 66

theorem OAI.AffineBernstein.maximal_model_uniform_log_cells line 92

Source documentation

Uniform actual sigma control in every translated logarithmic unit cell, from the original PDE, completeness, maximal-model normalization, and true coordinate covariance. There is no cell-mass hypothesis. Suitable regular base domains may be supplied later when applying the differential inequality.

theorem maximal_model_uniform_log_cells {n k m d : ℕ}
    (hn : 1 ≤ n) (hk : 1 ≤ k) (hm : 1 ≤ m)
    (e : Fin n ≃ Fin k ⊕ Fin d) (eE : Fin m ≃ Fin d ⊕ Unit)
    (f : WithLp 2 (Space d × ℝ) ≃ₗᵢ[ℝ] Space m)
    {Ω : Set (Space n)} (hΩ : IsOpen Ω) (hne : Ω.Nonempty) (hcv : Convex ℝ Ω)
    {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
    (hp : ∀ x ∈ Ω, (hessian u x).PosDef) (hmP : AffineMaximalOn Ω u)
    (hcomplete : EuclideanGraphComplete Ω u)
    (hmax : ∀ d' : ℕ, m = d'+1 → ∀ C' : Set (Space (k+1) × Space d'),
      IsModelShape C' → InAffineLimitFamily (sourceEpigraph Ω u) C' → False) :
    ∃ Cσ : ℝ, 0 ≤ Cσ ∧
      ∀ (C : Set (Space k × Space m)), IsModelShape C →
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.AffineMaximalOn, OAI.AffineBernstein.EuclideanGraphComplete, OAI.AffineBernstein.IsModelShape, OAI.AffineBernstein.InAffineLimitFamily, OAI.AffineBernstein.sourceEpigraph