Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Section5.Contracts.A8LeavesFields

Six relative fields of A8Remaining from the trace leaf #

gradient, material, jets, relative_initial, leading, temperature, each derived from a8Core and the corresponding producer. The trace premise hTr is the t1hTrace leaf of A8Leaves.

source
def AVenhance.Infra.Section5.Contracts.A8TraceLeaf (β C₀ : ℝ) :
Prop

The trace leaf (S amplitude, gate).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem AVenhance.Infra.Section5.Contracts.a8_gradient_of_trace (β C₀ : ℝ) (hTr : A8TraceLeaf β C₀) :
    ∃ (C : ℝ) (C₁ : ℝ), 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 → Integration.TGradientContract β (I.kappaSeq κ M (m - 1)) T C (√(I.kappaSeq κ M (m - 1)) * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θprev s) x))
    source
    theorem AVenhance.Infra.Section5.Contracts.a8_jets_of_trace (β C₀ : ℝ) (hTr : A8TraceLeaf β C₀) :
    ∃ (C : ℝ) (C₁ : ℝ), 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 → Integration.TPositiveJetsContract I m T C (√(I.kappaSeq κ M (m - 1)) * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θprev s) x))
    source
    theorem AVenhance.Infra.Section5.Contracts.a8_material_of_trace (β C₀ : ℝ) (hTr : A8TraceLeaf β C₀) :
    ∃ (C : ℝ) (C₁ : ℝ), 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 → Integration.TMaterialContract I Φ m (I.kappaSeq κ M (m - 1)) T C (√(I.kappaSeq κ M (m - 1)) * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θprev s) x))
    source
    theorem AVenhance.Infra.Section5.Contracts.a8_relative_initial_of_trace (β C₀ : ℝ) (hTr : A8TraceLeaf β C₀) :
    ∃ (C : ℝ) (C₁ : ℝ), 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 → Integration.InitialLayerContract I hΦ m (I.kappaSeq κ M m) θm T C (√(I.kappaSeq κ M (m - 1)) * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θprev s) x))
    source
    theorem AVenhance.Infra.Section5.Contracts.a8_leading_of_trace (β C₀ : ℝ) (hTr : A8TraceLeaf β C₀) :
    ∃ (C : ℝ) (C₁ : ℝ), 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 → Integration.LeadingErrorContract I hΦ m (I.kappaSeq κ M m) T C (√(I.kappaSeq κ M (m - 1)) * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θprev s) x))
    source
    theorem AVenhance.Infra.Section5.Contracts.a8_temperature_of_trace (β C₀ : ℝ) (hTr : A8TraceLeaf β C₀) :
    ∃ (C : ℝ) (C₁ : ℝ), 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 → Integration.TemperatureErrorContract I m (I.kappaSeq κ M (m - 1)) θprev T C (√(I.kappaSeq κ M (m - 1)) * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θprev s) x))