VertexIntegration.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Integrating the vertex amount

The actual finite terminal flow gives pointwise good-path domination on the large-mass region. Integrating that domination together with the small-mass estimate extracts the normalized vertex energy from its nonnegative amount. This is the finite nonnegative assembly in §11.

def OAI.LipschitzHilbert.goodPathSet line 27
def OAI.LipschitzHilbert.goodPathContribution line 29
theorem OAI.LipschitzHilbert.sum_goodPathContribution line 33

theorem OAI.LipschitzHilbert.vertex_amount_pointwise line 46

Source documentation

The two spatial mass regimes fit into one nonnegative pointwise bound.

theorem vertex_amount_pointwise (F : α → TerminalFlow κ ι N)
    (bad : α → Finset ι) (n V : α → ℝ) (h e Q : ι → α → ℝ) (M C : ℝ)
    (hC : 0 ≤ C) (hn : ∀ x, 0 ≤ n x)
    (hh : ∀ i x, 0 ≤ h i x) (hQ : ∀ i x, 0 ≤ Q i x)
    (hsmallMass : ∀ x, n x ≤ M → V x ≤ C * n x)
    (hV : ∀ x, M < n x → 0 < V x)
    (he : ∀ x, M < n x → ∀ i, e i x ≤ C * h i x)
    (hprob : ∀ x, M < n x → ∀ i, (F x).terminalProbability i = e i x * Q i x / V x)
    (hrate : ∀ x, M < n x → ∀ i, (F x).exitRate i ≤ C * h i x)
    (hbad : ∀ x, M < n x → C * ∑ i ∈ bad x, h i x ≤ 1 / 2) (x : α) :
    V x ≤ C * n x + 2 * C * ∑ i, goodPathContribution bad h Q i x := by
…

Mentions: OAI.LipschitzHilbert.TerminalFlow, OAI.LipschitzHilbert.goodPathContribution

theorem OAI.LipschitzHilbert.vertex_amount_integral line 72

Source documentation

Integrate the vertex amount from actual good-path contributions. The only analytic inputs are their proved restricted integral bounds.

theorem vertex_amount_integral (μ : Measure α) (F : α → TerminalFlow κ ι N)
    (bad : α → Finset ι) (n V : α → ℝ) (h e Q : ι → α → ℝ) (M C P : ℝ)
    (hC : 0 ≤ C)
    (hn : ∀ x, 0 ≤ n x) (hV0 : ∀ x, 0 ≤ V x)
    (hh : ∀ i x, 0 ≤ h i x) (hQ : ∀ i x, 0 ≤ Q i x)
    (hnmeas : AEStronglyMeasurable n μ) (hVmeas : AEStronglyMeasurable V μ)
    (hhint : ∀ i, Integrable (h i) μ) (hnmass : ∀ x, n x ≤ ∑ i, h i x)
    (hgood : ∀ i, MeasurableSet (goodPathSet bad i))
    (hpathInt : ∀ i, IntegrableOn (fun x => h i x * Q i x) (goodPathSet bad i) μ)
    (hpathBound : ∀ i, (∫ x in goodPathSet bad i, h i x * Q i x ∂μ) ≤ P * ∫ x, h i x ∂μ)
    (hsmallMass : ∀ x, n x ≤ M → V x ≤ C * n x)
    (hV : ∀ x, M < n x → 0 < V x)
…

Mentions: OAI.LipschitzHilbert.TerminalFlow, OAI.LipschitzHilbert.goodPathSet

def OAI.LipschitzHilbert.vertexAmount line 131
Source documentation
The actual vertex amount from §11.
```
def vertexAmount (n : ℝ) (A : E) (a p : ℝ) : ℝ := n + n ^ (a - p) * ‖A‖ ^ p
…
```
theorem OAI.LipschitzHilbert.normalized_vertex_energy_eq line 134

theorem OAI.LipschitzHilbert.normalized_vertex_energy_integrable line 146

Source documentation

Subtracting the integrable mass baseline extracts the normalized energy without any extra domination or measurability assumption on that energy.

theorem normalized_vertex_energy_integrable (μ : Measure α)
    (n : α → ℝ) (A : α → E) {a p : ℝ} (hn : ∀ x, 0 < n x) (hp : p ≠ 0)
    (hnint : Integrable n μ) (hVint : Integrable (fun x => vertexAmount (n x) (A x) a p) μ) :
    Integrable (fun x => ‖(n x ^ (a / p - 1)) • A x‖ ^ p) μ := by
…

Mentions: OAI.LipschitzHilbert.vertexAmount

theorem OAI.LipschitzHilbert.normalized_vertex_moment_le line 161

Source documentation

An integrated amount bound gives the desired vertex Lp energy bound.

theorem normalized_vertex_moment_le (μ : Measure α)
    (n : α → ℝ) (A : α → E) {a p T : ℝ} (hn : ∀ x, 0 < n x) (hp : 0 < p)
    (hnint : Integrable n μ) (hVint : Integrable (fun x => vertexAmount (n x) (A x) a p) μ)
    (hbound : (∫ x, vertexAmount (n x) (A x) a p ∂μ) ≤ T) :
    (∫ x, ‖(n x ^ (a / p - 1)) • A x‖ ^ p ∂μ) ^ (1 / p) ≤ T ^ (1 / p) := by
…

Mentions: OAI.LipschitzHilbert.vertexAmount