Quantifier-block combinators and amplitude monotonicity for the step-down estimate leaves

OnA8Instances is a long ∀ chain. This file packages the three moves used when assembling the seven relative fields from the θ-profile leaf: mapping a pointwise implication, applying an implication proved on the block to a premise proved on the block (thresholds combine by max), and passing from the big-bound premise block (no θ_m) to the step-down premise block. It also records the (elementary) monotonicity of the T-jet contracts in the coefficient A, and the scale inequality ε_{m-1}^{1+γ/2} ≤ R on the block.

@[reducible, inline]

abbrev AVenhance.Infra.Section5.Contracts.A8Pred (β : ℝ) : Type

The type of predicates over the step-down premise block.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev AVenhance.Infra.Section5.Contracts.relS {β : ℝ} (I : Ingredients β) (κ : ℝ) (M m : ℕ) (θprev : ℝ → Homogenization.Vec 2 → ℝ) : ℝ

The relative amplitude S = √κ_{m-1} · √‖∇θ_{m-1}‖².

Equations

• AVenhance.Infra.Section5.Contracts.relS I κ M m θprev = √(I.kappaSeq κ M (m - 1)) * √(AVenhance.spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => AVenhance.spaceGrad (θprev s) x)

theorem AVenhance.Infra.Section5.Contracts.relS_nonneg {β : ℝ} (I : Ingredients β) (κ : ℝ) (M m : ℕ) (θprev : ℝ → Homogenization.Vec 2 → ℝ) : 0 ≤ relS I κ M m θprev

theorem AVenhance.Infra.Section5.Contracts.OnA8Instances.map {β C₀ C₁ : ℝ} {P Q : A8Pred β} (h : Integration.OnA8Instances β C₀ C₁ P) (f : ∀ (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ) (κ : ℝ) (M : ℕ) (R : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (θm θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ), P I Φ hΦ κ M R θ₀ m θm θprev T → Q I Φ hΦ κ M R θ₀ m θm θprev T) : Integration.OnA8Instances β C₀ C₁ Q

Pointwise implication between block predicates.

theorem AVenhance.Infra.Section5.Contracts.OnA8Instances.map_R {β C₀ C₁ : ℝ} {P Q : A8Pred β} (h : Integration.OnA8Instances β C₀ C₁ P) (f : ∀ (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ) (κ : ℝ) (M : ℕ) (R : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (θm θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ), 0 < R → mTheta0 β I.Λ R ≤ m → P I Φ hΦ κ M R θ₀ m θm θprev T → Q I Φ hΦ κ M R θ₀ m θm θprev T) : Integration.OnA8Instances β C₀ C₁ Q

Pointwise implication that may use the radius and the cutoff index of the block.

theorem AVenhance.Infra.Section5.Contracts.OnA8Instances.map₂ {β C₀ C₁ C₂ : ℝ} {P Q Z : A8Pred β} (hP : Integration.OnA8Instances β C₀ C₁ P) (hQ : Integration.OnA8Instances β C₀ C₂ Q) (f : ∀ (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ) (κ : ℝ) (M : ℕ) (R : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (θm θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ), P I Φ hΦ κ M R θ₀ m θm θprev T → Q I Φ hΦ κ M R θ₀ m θm θprev T → Z I Φ hΦ κ M R θ₀ m θm θprev T) : Integration.OnA8Instances β C₀ (max C₁ C₂) Z

Two-premise pointwise implication on the block.

theorem AVenhance.Infra.Section5.Contracts.OnA8Instances.and {β C₀ C₁ C₂ : ℝ} {P Q : A8Pred β} (hP : Integration.OnA8Instances β C₀ C₁ P) (hQ : Integration.OnA8Instances β C₀ C₂ Q) : Integration.OnA8Instances β C₀ (max C₁ C₂) fun (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ) (κ : ℝ) (M : ℕ) (R : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (θm θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) => P I Φ hΦ κ M R θ₀ m θm θprev T ∧ Q I Φ hΦ κ M R θ₀ m θm θprev T

Conjunction on the block.

theorem AVenhance.Infra.Section5.Contracts.OnA8Instances.of_A7 {β C₀ C₁ : ℝ} {P : (I : Ingredients β) → (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) → IsStreamSeq I Φ → ℝ → ℕ → ℝ → (Homogenization.Vec 2 → ℝ) → ℕ → (ℝ → Homogenization.Vec 2 → ℝ) → (ℕ → ℝ → Homogenization.Vec 2 → ℝ) → Prop} (h : Integration.OnA7Instances β C₀ C₁ P) : Integration.OnA8Instances β C₀ C₁ fun (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ) (κ : ℝ) (M : ℕ) (R : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (_θm θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) => P I Φ hΦ κ M R θ₀ m θprev T

A big-bound premise block statement is a step-down premise-block statement that ignores θ_m.

theorem AVenhance.Infra.Section5.Contracts.OnA8Instances.of_A7_forall {β C₀ C₁ : ℝ} {Q : (I : Ingredients β) → (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) → IsStreamSeq I Φ → ℝ → ℕ → ℝ → (Homogenization.Vec 2 → ℝ) → ℕ → (ℝ → Homogenization.Vec 2 → ℝ) → (ℕ → ℝ → Homogenization.Vec 2 → ℝ) → ℝ → Prop} (h : Integration.OnA7Instances β C₀ C₁ fun (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ) (κ : ℝ) (M : ℕ) (R : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) => ∀ (B : ℝ), 0 ≤ B → Q I Φ hΦ κ M R θ₀ m θprev T B) : Integration.OnA8Instances β C₀ C₁ fun (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ) (κ : ℝ) (M : ℕ) (R : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (_θm θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) => Q I Φ hΦ κ M R θ₀ m θprev T (relS I κ M m θprev)

Specialize a big-bound premise block family ∀ B ≥ 0, Q B to the relative amplitude S.

theorem AVenhance.Infra.Section5.Contracts.OnA8Instances.gate_mp {β C₀ C₁ C₂ : ℝ} {P Q : A8Pred β} (hPQ : Integration.OnA8Instances β C₀ C₁ fun (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ) (κ : ℝ) (M : ℕ) (R : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (θm θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) => P I Φ hΦ κ M R θ₀ m θm θprev T → Q I Φ hΦ κ M R θ₀ m θm θprev T) (hP : Integration.OnA8Instances β C₀ C₂ fun (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ) (κ : ℝ) (M : ℕ) (R : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (θm θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) => 6 / 5 ≤ β → epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2 - delta β) ≤ R → P I Φ hΦ κ M R θ₀ m θm θprev T) : Integration.OnA8Instances β C₀ (max C₁ C₂) fun (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ) (κ : ℝ) (M : ℕ) (R : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (θm θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) => 6 / 5 ≤ β → epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2 - delta β) ≤ R → Q I Φ hΦ κ M R θ₀ m θm θprev T

Modus ponens under the gate: an ungated implication on the block applied to a gated premise gives a gated conclusion.

theorem AVenhance.Infra.Section5.Contracts.OnA8Instances.gate_and {β C₀ C₁ C₂ : ℝ} {P Q : A8Pred β} (hP : Integration.OnA8Instances β C₀ C₁ fun (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ) (κ : ℝ) (M : ℕ) (R : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (θm θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) => 6 / 5 ≤ β → epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2 - delta β) ≤ R → P I Φ hΦ κ M R θ₀ m θm θprev T) (hQ : Integration.OnA8Instances β C₀ C₂ fun (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ) (κ : ℝ) (M : ℕ) (R : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (θm θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) => 6 / 5 ≤ β → epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2 - delta β) ≤ R → Q I Φ hΦ κ M R θ₀ m θm θprev T) : Integration.OnA8Instances β C₀ (max C₁ C₂) fun (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ) (κ : ℝ) (M : ℕ) (R : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (θm θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) => 6 / 5 ≤ β → epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2 - delta β) ≤ R → P I Φ hΦ κ M R θ₀ m θm θprev T ∧ Q I Φ hΦ κ M R θ₀ m θm θprev T

Conjunction under the gate.

theorem AVenhance.Infra.Section5.Contracts.OnA8Instances.gate_map {β C₀ C₁ : ℝ} {P Q : A8Pred β} (h : Integration.OnA8Instances β C₀ C₁ fun (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ) (κ : ℝ) (M : ℕ) (R : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (θm θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) => 6 / 5 ≤ β → epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2 - delta β) ≤ R → P I Φ hΦ κ M R θ₀ m θm θprev T) (f : ∀ (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ) (κ : ℝ) (M : ℕ) (R : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (θm θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ), P I Φ hΦ κ M R θ₀ m θm θprev T → Q I Φ hΦ κ M R θ₀ m θm θprev T) : Integration.OnA8Instances β C₀ C₁ fun (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ) (κ : ℝ) (M : ℕ) (R : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (θm θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) => 6 / 5 ≤ β → epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2 - delta β) ≤ R → Q I Φ hΦ κ M R θ₀ m θm θprev T

Pointwise implication under the gate.

Scales on the block

theorem AVenhance.Infra.Section5.Contracts.epsilon_radius_le_of_mTheta0 {β : ℝ} (I : Ingredients β) {R : ℝ} (hR : 0 < R) {m : ℕ} (hm : mTheta0 β I.Λ R ≤ m) : epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2) ≤ R

ε_{m-1}^{1+γ/2} ≤ R for m ≥ m_θ₀(R).

theorem AVenhance.Infra.Section5.Contracts.OnA8Instances.radius (β C₀ : ℝ) : Integration.OnA8Instances β C₀ 0 fun (I : Ingredients β) (_Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (_hΦ : IsStreamSeq I _Φ) (_κ : ℝ) (_M : ℕ) (R : ℝ) (_θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (_θm _θprev : ℝ → Homogenization.Vec 2 → ℝ) (_T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) => epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2) ≤ R

The radius scale holds on the whole step-down premise block.

Monotonicity of the V-increment contract in the profile constant

theorem AVenhance.Infra.Section5.Contracts.A8LeavesTools.iterateAmplitude_mono {η η' : ℝ} (hη : 0 ≤ η) (hle : η ≤ η') (i : ℕ) : Section4.iterateAmplitude η i ≤ Section4.iterateAmplitude η' i

theorem AVenhance.Infra.Section5.Contracts.A8LeavesTools.iterateAmplitude_nonneg' {η : ℝ} (hη : 0 ≤ η) (i : ℕ) : 0 ≤ Section4.iterateAmplitude η i

theorem AVenhance.Infra.Section5.Contracts.vIncrementContract_mono {β : ℝ} {I : Ingredients β} {m : ℕ} {κ Cs Cs' R N : ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (h : Integration.VIncrementContract I m κ T Cs R N) (hCs : 0 ≤ Cs) (hle : Cs ≤ Cs') (hR : 0 < R) (hN : 0 ≤ N) : Integration.VIncrementContract I m κ T Cs' R N

Monotonicity of the T-jet contracts in the coefficient

theorem AVenhance.Infra.Section5.Contracts.tGradientContract_mono {β κ A A' S : ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (h : Integration.TGradientContract β κ T A S) (hAA : A ≤ A') (hS : 0 ≤ S) : Integration.TGradientContract β κ T A' S

theorem AVenhance.Infra.Section5.Contracts.tPositiveJetsContract_mono {β : ℝ} {I : Ingredients β} {m : ℕ} {A A' S : ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (h : Integration.TPositiveJetsContract I m T A S) (hA : 0 ≤ A) (hAA : A ≤ A') (hS : 0 ≤ S) : Integration.TPositiveJetsContract I m T A' S

theorem AVenhance.Infra.Section5.Contracts.firstOrderGradJetContract_mono {β : ℝ} {I : Ingredients β} {m : ℕ} {κ A A' S : ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (h : Integration.FirstOrderGradJetContract I m κ T A S) (hA : 0 ≤ A) (hAA : A ≤ A') (hS : 0 ≤ S) : Integration.FirstOrderGradJetContract I m κ T A' S

theorem AVenhance.Infra.Section5.Contracts.secondOrderGradJetContract_mono {β : ℝ} {I : Ingredients β} {m : ℕ} {κ A A' S : ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (h : Integration.SecondOrderGradJetContract I m κ T A S) (hA : 0 ≤ A) (hAA : A ≤ A') (hS : 0 ≤ S) : Integration.SecondOrderGradJetContract I m κ T A' S