ConeTopology.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Compact normalized monomial cones

Local algebra for uniform Cartier sections.

lemma OAI.CartierSections.FormalMonomial.exists_finite_formula line 24
Source documentation
A single finite subset of the support computes all nonnegative weighted orders, including all faces. The exponents do not depend on the weights.
```
lemma exists_finite_formula (f : MvPowerSeries σ k) :
    ∃ T : Finset (σ →₀ ℕ), ∀ w : σ → NNReal,
      value w f = T.inf (fun d => (Finsupp.weight w d : ENNReal)) := by
…
```
Mentions: OAI.CartierSections.FormalMonomial.value
lemma OAI.CartierSections.FormalMonomial.continuous_weight line 36
lemma OAI.CartierSections.FormalMonomial.continuous_value line 42
Source documentation
Formal monomial evaluation is continuous on the closed cone of nonnegative weights.
```
lemma continuous_value (f : MvPowerSeries σ k) :
    Continuous (fun w : σ → NNReal => value w f) := by
…
```
Mentions: OAI.CartierSections.FormalMonomial.value
lemma OAI.CartierSections.continuous_monomial_evaluation line 53
lemma OAI.CartierSections.continuous_monomial_evaluations line 59
Source documentation
We use the pointwise topology on actual regular-function evaluations, which is precisely the topology invoked in the E compactness argument.
```
lemma continuous_monomial_evaluations (θ : A →ₐ[k] MvPowerSeries σ k) :
    Continuous (fun w : σ → NNReal => fun f : A => expansionValuation θ w f) :=
…
```
Mentions: OAI.CartierSections.expansionValuation
def OAI.CartierSections.normalizedWeights line 65
Source documentation
The normalized section of a monomial cone; a i is the positive discrepancy of its primitive ray in the application.
```
def normalizedWeights (a : σ → NNReal) : Set (σ → NNReal) :=
…
```
lemma OAI.CartierSections.isClosed_normalizedWeights line 68
lemma OAI.CartierSections.isCompact_normalizedWeights line 73
lemma OAI.CartierSections.isCompact_monomial_cone line 87
Source documentation
The normalized monomial cone is compact in pointwise regular-function evaluation.
```
lemma isCompact_monomial_cone (θ : A →ₐ[k] MvPowerSeries σ k)
    (a : σ → NNReal) (ha : ∀ i, 0 < a i) :
    IsCompact ((fun w : σ → NNReal => fun f : A => expansionValuation θ w f) ''
      normalizedWeights a) :=
…
```
Mentions: OAI.CartierSections.expansionValuation, OAI.CartierSections.normalizedWeights
def OAI.CartierSections.valuationConstraints line 104
Source documentation
Literal evaluation constraints from the common lc slice, on the ambient space of readings of regular functions. In use m j is the positive integer multiplicity from E, and the normalization of discrepancy is imposed by the normalized coordinate cone.
```
def valuationConstraints (h : A) (F : J → A) (m : J → ENNReal) : Set (A → ENNReal) :=
…
```
lemma OAI.CartierSections.isClosed_valuationConstraints line 108

def OAI.CartierSections.finiteChartSlice line 114

Source documentation

A finite union of formal-coordinate cones cut by normalized evaluation constraints.

def finiteChartSlice (θ : ι → A →ₐ[k] MvPowerSeries σ k)
    (a : ι → σ → NNReal) (h : A) (F : J → A) (m : J → ENNReal) : Set (A → ENNReal) :=
…

lemma OAI.CartierSections.isCompact_finiteChartSlice line 119

lemma OAI.CartierSections.simultaneous_targets_of_finite line 128

Source documentation

Compactness turns simultaneous domination on every finite set of functions into domination on all functions.

lemma simultaneous_targets_of_finite (θ : ι → A →ₐ[k] MvPowerSeries σ k)
    (a : ι → σ → NNReal) (ha : ∀ i j, 0 < a i j)
    (h : A) (F : J → A) (m : J → ENNReal) (s : A → ENNReal)
    (hfinite : ∀ T : Finset A, ∃ (i : ι) (w : σ → NNReal),
      w ∈ normalizedWeights (a i) ∧
      (fun f => expansionValuation (θ i) w f) ∈ valuationConstraints h F m ∧
      ∀ f ∈ T, s f ≤ expansionValuation (θ i) w f) :
    ∃ (i : ι) (w : σ → NNReal), w ∈ normalizedWeights (a i) ∧
      (fun f => expansionValuation (θ i) w f) ∈ valuationConstraints h F m ∧
      ∀ f, s f ≤ expansionValuation (θ i) w f := by
…

Mentions: OAI.CartierSections.normalizedWeights, OAI.CartierSections.expansionValuation, OAI.CartierSections.valuationConstraints