Related estimates used together by the same construction modules.
A slow base whose cutoffs are aligned with the natural entrance #
The retained local hierarchy extends strictly beyond the natural entrance. Its cutoff transition lies inside the proved initial true-cone collar and before the finite modulation begins. The same finite base, local hierarchy, and five-row exterior repair are used throughout.
noncomputable def
NavierStokes.EntranceAlignedBase.trueWidth
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
:
True width, given by H.initial.choose.
Equations
Instances For
theorem
NavierStokes.EntranceAlignedBase.trueWidth_pos
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
:
theorem
NavierStokes.EntranceAlignedBase.trueWidth_spec
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{y eta : ℝ}
(hy : 0 < y)
(ht : y ≤ trueWidth W H)
(heta : eta ∈ HeatedOutgoing.parameterDomain)
:
noncomputable def
NavierStokes.EntranceAlignedBase.analyticEnd
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
:
Analytic end, given by NominalConeAssembly.activeLeft W * Real.exp W.controls.referenceWidth.
Equations
Instances For
noncomputable def
NavierStokes.EntranceAlignedBase.windowCap
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
(lo : ℝ)
:
Window cap, given by min lo (min (NominalConeAssembly.activeLeft W * Real.exp (trueWidth W H)) (analyticEnd W)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NavierStokes.EntranceAlignedBase.zeroEnd
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
(lo : ℝ)
:
Zero end, given by NominalConeAssembly.activeLeft W + (windowCap W H lo - NominalConeAssembly.activeLeft W) / 4.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NavierStokes.EntranceAlignedBase.cutoffInner
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
(lo : ℝ)
:
Cutoff inner, given by NominalConeAssembly.activeLeft W + (windowCap W H lo - NominalConeAssembly.activeLeft W) / 2.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NavierStokes.EntranceAlignedBase.cutoffStop
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
(lo : ℝ)
:
Cutoff stop, given by NominalConeAssembly.activeLeft W + 3 * (windowCap W H lo - NominalConeAssembly.activeLeft W) / 4.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.EntranceAlignedBase.entrance_lt_cap
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{lo : ℝ}
(hlo : NominalConeAssembly.activeLeft W < lo)
:
theorem
NavierStokes.EntranceAlignedBase.window_order
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{lo : ℝ}
(hlo : NominalConeAssembly.activeLeft W < lo)
:
NominalConeAssembly.activeLeft W < zeroEnd W H lo ∧ zeroEnd W H lo < cutoffInner W H lo ∧ cutoffInner W H lo < cutoffStop W H lo ∧ cutoffStop W H lo < windowCap W H lo
theorem
NavierStokes.EntranceAlignedBase.cutoffStop_lt_lo
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{lo : ℝ}
(hlo : NominalConeAssembly.activeLeft W < lo)
:
theorem
NavierStokes.EntranceAlignedBase.cutoffStop_lt_trueEnd
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{lo : ℝ}
(hlo : NominalConeAssembly.activeLeft W < lo)
:
theorem
NavierStokes.EntranceAlignedBase.cutoffStop_lt_analyticEnd
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{lo : ℝ}
(hlo : NominalConeAssembly.activeLeft W < lo)
:
theorem
NavierStokes.EntranceAlignedBase.cutoffInner_pos
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{lo : ℝ}
(hlo : NominalConeAssembly.activeLeft W < lo)
:
theorem
NavierStokes.EntranceAlignedBase.zeroEnd_pos
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{lo : ℝ}
(hlo : NominalConeAssembly.activeLeft W < lo)
:
theorem
NavierStokes.EntranceAlignedBase.cutoffStop_lt_radius
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{lo : ℝ}
(hlo : NominalConeAssembly.activeLeft W < lo)
:
theorem
NavierStokes.EntranceAlignedBase.cutoffStop_lt_patch
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{lo : ℝ}
(hlo : NominalConeAssembly.activeLeft W < lo)
:
cutoffStop W H lo < ReservedPatches.radialLeft F W.controls.radius ReservedPatches.Slot.positive ^ 2 / 2
theorem
NavierStokes.EntranceAlignedBase.cutoff_transition_true
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{lo : ℝ}
(hlo : NominalConeAssembly.activeLeft W < lo)
{p : ℝ × ℝ}
(hp : p.1 ∈ Set.Icc (cutoffInner W H lo) (cutoffStop W H lo))
(heta : p.2 ∈ HeatedOutgoing.parameterDomain)
:
The whole cutoff transition is inside the actual initial true collar.
noncomputable def
NavierStokes.EntranceAlignedBase.scheme
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
:
A new actual global recursion, retaining the same local hierarchy through the entrance and changing only its common seed cutoff.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.EntranceAlignedBase.localization
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
:
GlobalSlowProfiles.Localization (scheme W H Q M hlo) (AssembledSlowBase.nominalHierarchy W) (cutoffInner W H lo)
theorem
NavierStokes.EntranceAlignedBase.scheme_base
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
:
theorem
NavierStokes.EntranceAlignedBase.scheme_outer
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
:
theorem
NavierStokes.EntranceAlignedBase.scheme_base_beta
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
:
theorem
NavierStokes.EntranceAlignedBase.nominal_ACT_fields
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
{X eta : ℝ}
(hX : 0 ≤ X)
(hc : X ≤ analyticEnd W)
(heta : eta ∈ ReferencePath.parameterInterval)
:
The actual nominal fields agree with the ACT fields throughout the analytic collar, rather than only on the smaller natural core.
theorem
NavierStokes.EntranceAlignedBase.modified_ACT_fields
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
{p : ℝ × ℝ}
(hX : 0 ≤ p.1)
(hc : p.1 < cutoffInner W H lo)
(heta : p.2 ∈ S)
:
theorem
NavierStokes.EntranceAlignedBase.modified_ACT_pressure
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
{p : ℝ × ℝ}
(hX : 0 ≤ p.1)
(hc : p.1 < cutoffInner W H lo)
(heta : p.2 ∈ S)
:
theorem
NavierStokes.EntranceAlignedBase.base_phi_axial_pressure
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
{p : ℝ × ℝ}
(hX : 0 ≤ p.1)
(hc : p.1 < cutoffInner W H lo)
(heta : p.2 ∈ S)
:
GlobalSlowProfiles.xProfile (scheme W H Q M hlo).base.phi p = SlowRecursion.profile ((AssembledSlowBase.nominalHierarchy W).coefficients 0 0) p ∧ GlobalSlowProfiles.xProfile (scheme W H Q M hlo).base.axial p = SlowRecursion.profile ((AssembledSlowBase.nominalHierarchy W).coefficients 0 1) p ∧ GlobalSlowProfiles.xProfile (scheme W H Q M hlo).base.pressure p = SlowRecursion.profile ((AssembledSlowBase.nominalHierarchy W).coefficients 0 3) p
theorem
NavierStokes.EntranceAlignedBase.base_beta_pos
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
{p : ℝ × ℝ}
(hX : 0 < p.1)
(hc : p.1 < cutoffInner W H lo)
(heta : p.2 ∈ S)
:
GlobalSlowProfiles.xProfile (scheme W H Q M hlo).base.beta p = SlowRecursion.profile ((AssembledSlowBase.nominalHierarchy W).coefficients 0 4) p
theorem
NavierStokes.EntranceAlignedBase.base_beta_axis
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
{eta : ℝ}
(heta : eta ∈ S)
:
theorem
NavierStokes.EntranceAlignedBase.baseAgreement
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
:
GlobalSlowProfiles.BaseAgreement (scheme W H Q M hlo) (AssembledSlowBase.nominalHierarchy W) (cutoffInner W H lo)
theorem
NavierStokes.EntranceAlignedBase.small_lt_cutoffInner
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{lo : ℝ}
(hlo : NominalConeAssembly.activeLeft W < lo)
:
theorem
NavierStokes.EntranceAlignedBase.smallLocalization
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
:
The extension constructor may use a small natural core independently of the larger radius retained by the actual seed cutoff.
theorem
NavierStokes.EntranceAlignedBase.smallBaseAgreement
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
:
theorem
NavierStokes.EntranceAlignedBase.zero_coefficients
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
{p : ℝ × ℝ}
(hX : 0 < p.1)
(he : p.1 < NominalConeAssembly.activeLeft W)
(heta : p.2 ∈ S)
:
SlowExpansionResidual.angularCoefficient F.data.h (GlobalSlowProfiles.asSlowProfiles (scheme W H Q M hlo)) 0 p = 0 ∧ SlowExpansionResidual.axialCoefficient F.data.h (GlobalSlowProfiles.asSlowProfiles (scheme W H Q M hlo)) 0 p = 0
The order-zero equations hold on the full natural core, up to the entrance from below. They are obtained from the actual natural solution.
theorem
NavierStokes.EntranceAlignedBase.smallZeroOrder
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
:
AssembledSlowBase.ZeroOrderSolved (scheme W H Q M hlo) (AssembledSlowBase.nominalInner W)
noncomputable def
NavierStokes.EntranceAlignedBase.alignedCoefficients
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
:
Aligned coefficients, given by coefficients (smallLocalization W H Q M hlo) (smallBaseAgreement W H Q M hlo) (smallZeroOrder W H Q M hlo) M.contains.
Equations
Instances For
theorem
NavierStokes.EntranceAlignedBase.aligned_smooth
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
:
SlowBorelBase.SmoothCoefficients (alignedCoefficients W H Q M hlo)
theorem
NavierStokes.EntranceAlignedBase.aligned_coefficientMatches
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
:
BasePrefixIdentity.CoefficientMatches F.data.h W.axis.normalization (alignedCoefficients W H Q M hlo)
(GlobalSlowProfiles.asSlowProfiles (scheme W H Q M hlo))
theorem
NavierStokes.EntranceAlignedBase.positive_coefficients_zero
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
{n : ℕ}
(hn : 0 < n)
{p : ℝ × ℝ}
(hX : 0 < p.1)
(hc : p.1 < cutoffInner W H lo)
(heta : p.2 ∈ S)
:
SlowExpansionResidual.angularCoefficient F.data.h (GlobalSlowProfiles.asSlowProfiles (scheme W H Q M hlo)) n p = 0 ∧ SlowExpansionResidual.axialCoefficient F.data.h (GlobalSlowProfiles.asSlowProfiles (scheme W H Q M hlo)) n p = 0
theorem
NavierStokes.EntranceAlignedBase.positive_densities_zero
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
{n : ℕ}
(hn : 0 < n)
{R eta : ℝ}
(hR : R ∈ Set.Icc 0 √(2 * zeroEnd W H lo))
(heta : eta ∈ S)
:
SlowResidualMatching.thetaDensity F.data.h W.axis.normalization (GlobalSlowProfiles.asSlowProfiles (scheme W H Q M hlo))
n (R, eta) = 0 ∧ SlowResidualMatching.zDensity F.data.h (GlobalSlowProfiles.asSlowProfiles (scheme W H Q M hlo)) n (R, eta) = 0
theorem
NavierStokes.EntranceAlignedBase.positive_raw_stresses_zero
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
{n : ℕ}
(hn : 0 < n)
{R eta : ℝ}
(hR : R ≤ √(2 * zeroEnd W H lo))
(heta : eta ∈ S)
:
SlowStressSupport.stress 2
(SlowResidualMatching.thetaDensity F.data.h W.axis.normalization
(GlobalSlowProfiles.asSlowProfiles (scheme W H Q M hlo)) n)
(R, eta) = 0 ∧ SlowStressSupport.stress 1
(SlowResidualMatching.zDensity F.data.h (GlobalSlowProfiles.asSlowProfiles (scheme W H Q M hlo)) n) (R, eta) = 0
theorem
NavierStokes.EntranceAlignedBase.natural_densities_zero
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
{R eta : ℝ}
(hR : R ∈ Set.Icc 0 √(2 * NominalConeAssembly.activeLeft W))
(heta : eta ∈ S)
:
SlowResidualMatching.thetaDensity F.data.h W.axis.normalization (GlobalSlowProfiles.asSlowProfiles (scheme W H Q M hlo))
0 (R, eta) = 0 ∧ SlowResidualMatching.zDensity F.data.h (GlobalSlowProfiles.asSlowProfiles (scheme W H Q M hlo)) 0 (R, eta) = 0
Continuity supplies the natural entrance endpoint itself.
theorem
NavierStokes.EntranceAlignedBase.natural_raw_stresses_zero
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
{R eta : ℝ}
(hR : R ≤ √(2 * NominalConeAssembly.activeLeft W))
(heta : eta ∈ S)
:
SlowStressSupport.stress 2
(SlowResidualMatching.thetaDensity F.data.h W.axis.normalization
(GlobalSlowProfiles.asSlowProfiles (scheme W H Q M hlo)) 0)
(R, eta) = 0 ∧ SlowStressSupport.stress 1
(SlowResidualMatching.zDensity F.data.h (GlobalSlowProfiles.asSlowProfiles (scheme W H Q M hlo)) 0) (R, eta) = 0
theorem
NavierStokes.EntranceAlignedBase.extendCoreZero_zero_prefix
{T : Set ℝ}
(w : ParametricRadialExtension.ParameterWindow T)
{core bound : ℝ}
(hcore : 0 < core)
(f : GlobalSlowProfiles.EvenProfile T)
(hz : ∀ eta ∈ T, ∀ R ∈ Set.Icc 0 √(2 * bound), ↑f (R, eta) = 0)
{p : ℝ × ℝ}
(hp : p.1 ≤ bound)
:
The positive half-plane extension preserves a zero radial prefix for all parameters, including those handled by the fixed parameter retraction.
theorem
NavierStokes.EntranceAlignedBase.aligned_positive_stress_zero
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
{n : ℕ}
(hn : 0 < n)
{p : ℝ × ℝ}
(hp : p.1 ≤ zeroEnd W H lo)
:
(alignedCoefficients W H Q M hlo).stressTheta n p = 0 ∧ (alignedCoefficients W H Q M hlo).stressAxial n p = 0
Every positive stress coefficient vanishes strictly past the natural entrance, with one order-independent endpoint.
theorem
NavierStokes.EntranceAlignedBase.aligned_natural_stress_zero
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
{p : ℝ × ℝ}
(hp : p.1 ≤ NominalConeAssembly.activeLeft W)
:
(alignedCoefficients W H Q M hlo).stressTheta 0 p = 0 ∧ (alignedCoefficients W H Q M hlo).stressAxial 0 p = 0
theorem
NavierStokes.EntranceAlignedBase.aligned_stress_zero_left
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
(n : ℕ)
{p : ℝ × ℝ}
(hp : p.1 ≤ NominalConeAssembly.activeLeft W)
:
(alignedCoefficients W H Q M hlo).stressTheta n p = 0 ∧ (alignedCoefficients W H Q M hlo).stressAxial n p = 0
The entire actual coefficient family is stress-free through the entrance. No support conclusion is an input to this theorem.
theorem
NavierStokes.EntranceAlignedBase.aligned_stressZeroCore
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
:
BaseResidual.StressZeroCore (alignedCoefficients W H Q M hlo) (NominalConeAssembly.activeLeft W)
theorem
NavierStokes.EntranceAlignedBase.aligned_stress_zero_right
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
{n : ℕ}
(hn : 2 ≤ n)
{p : ℝ × ℝ}
(hp : AssembledSlowBase.nominalOuterX W ≤ p.1)
:
(alignedCoefficients W H Q M hlo).stressTheta n p = 0 ∧ (alignedCoefficients W H Q M hlo).stressAxial n p = 0
theorem
NavierStokes.EntranceAlignedBase.aligned_higher_support
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
{n : ℕ}
(hn : 2 ≤ n)
:
(tsupport fun (p : SlowBorelBase.Inner) =>
((alignedCoefficients W H Q M hlo).stressTheta n p, (alignedCoefficients W H Q M hlo).stressAxial n p)) ⊆
Set.Icc (zeroEnd W H lo) (AssembledSlowBase.nominalOuterX W) ×ˢ Set.Icc (-(AssembledSlowBase.commonWindow (scheme W H Q M hlo) ⋯).outer)
(AssembledSlowBase.commonWindow (scheme W H Q M hlo) ⋯).outer
theorem
NavierStokes.EntranceAlignedBase.aligned_higherInteriorSupport
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
:
theorem
NavierStokes.EntranceAlignedBase.zero_fields_eq
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
:
(GlobalSlowProfiles.asSlowProfiles (scheme W H Q M hlo)).phi 0 = (GlobalSlowProfiles.asSlowProfiles (AssembledSlowBase.modifiedScheme W Q M)).phi 0 ∧ (GlobalSlowProfiles.asSlowProfiles (scheme W H Q M hlo)).axial 0 = (GlobalSlowProfiles.asSlowProfiles (AssembledSlowBase.modifiedScheme W Q M)).axial 0 ∧ (GlobalSlowProfiles.asSlowProfiles (scheme W H Q M hlo)).flux 0 = (GlobalSlowProfiles.asSlowProfiles (AssembledSlowBase.modifiedScheme W Q M)).flux 0 ∧ (GlobalSlowProfiles.asSlowProfiles (scheme W H Q M hlo)).pressure 0 = (GlobalSlowProfiles.asSlowProfiles (AssembledSlowBase.modifiedScheme W Q M)).pressure 0
theorem
NavierStokes.EntranceAlignedBase.zero_residuals_eq
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
(p : ℝ × ℝ)
:
SlowExpansionResidual.angularCoefficient F.data.h (GlobalSlowProfiles.asSlowProfiles (scheme W H Q M hlo)) 0 p = SlowExpansionResidual.angularCoefficient F.data.h
(GlobalSlowProfiles.asSlowProfiles (AssembledSlowBase.modifiedScheme W Q M)) 0 p ∧ SlowExpansionResidual.axialCoefficient F.data.h (GlobalSlowProfiles.asSlowProfiles (scheme W H Q M hlo)) 0 p = SlowExpansionResidual.axialCoefficient F.data.h
(GlobalSlowProfiles.asSlowProfiles (AssembledSlowBase.modifiedScheme W Q M)) 0 p
theorem
NavierStokes.EntranceAlignedBase.zero_raw_stresses_eq
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
(R eta : ℝ)
:
SlowStressSupport.stress 2
(SlowResidualMatching.thetaDensity F.data.h W.axis.normalization
(GlobalSlowProfiles.asSlowProfiles (scheme W H Q M hlo)) 0)
(R, eta) = SlowStressSupport.stress 2
(SlowResidualMatching.thetaDensity F.data.h W.axis.normalization
(GlobalSlowProfiles.asSlowProfiles (AssembledSlowBase.modifiedScheme W Q M)) 0)
(R, eta) ∧ SlowStressSupport.stress 1
(SlowResidualMatching.zDensity F.data.h (GlobalSlowProfiles.asSlowProfiles (scheme W H Q M hlo)) 0) (R, eta) = SlowStressSupport.stress 1
(SlowResidualMatching.zDensity F.data.h
(GlobalSlowProfiles.asSlowProfiles (AssembledSlowBase.modifiedScheme W Q M)) 0)
(R, eta)
theorem
NavierStokes.EntranceAlignedBase.aligned_zero_stresses_eq
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
{p : ℝ × ℝ}
(hX : 0 ≤ p.1)
(heta : |p.2| ≤ 1)
:
(alignedCoefficients W H Q M hlo).stressTheta 0 p = (AssembledSlowBase.modifiedCoefficients W Q M).stressTheta 0 p ∧ (alignedCoefficients W H Q M hlo).stressAxial 0 p = (AssembledSlowBase.modifiedCoefficients W Q M).stressAxial 0 p
Moving the positive-order cutoff preserves the leading stress itself, including its actual integration constant.
theorem
NavierStokes.EntranceAlignedBase.leading_histories_eq
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
:
Set.EqOn (GlobalStressSupport.angularHistory (scheme W H Q M hlo) 0)
(GlobalStressSupport.angularHistory (AssembledSlowBase.modifiedScheme W Q M) 0) (Set.univ ×ˢ S) ∧ Set.EqOn (GlobalStressSupport.axialHistory (scheme W H Q M hlo) 0)
(GlobalStressSupport.axialHistory (AssembledSlowBase.modifiedScheme W Q M) 0) (Set.univ ×ˢ S)
theorem
NavierStokes.EntranceAlignedBase.aligned_zero_fields
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
{p : ℝ × ℝ}
(hX : 0 ≤ p.1)
(heta : |p.2| ≤ 1)
:
(alignedCoefficients W H Q M hlo).phi 0 p = W.axis.normalization * Q.f p ∧ (alignedCoefficients W H Q M hlo).axial 0 p = Q.U p ∧ (alignedCoefficients W H Q M hlo).pressure 0 p = Q.pressure p
The physical leading velocity and pressure are unchanged.
theorem
NavierStokes.EntranceAlignedBase.aligned_leading_axis
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
{eta : ℝ}
(heta : eta ∈ Set.Icc (-1) 1)
:
theorem
NavierStokes.EntranceAlignedBase.aligned_positive_axis
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
{n : ℕ}
(hn : 0 < n)
{eta : ℝ}
(heta : |eta| ≤ 1)
:
theorem
NavierStokes.EntranceAlignedBase.aligned_moments_zero
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
{n : ℕ}
(hn : 0 < n)
{eta : ℝ}
(heta : eta ∈ S)
:
(PositiveOrderMoments.moments n (PositiveOrderMoments.slice (GlobalStressSupport.axialHistory (scheme W H Q M hlo)) eta)
(PositiveOrderMoments.slice (GlobalStressSupport.angularHistory (scheme W H Q M hlo)) eta) fun (R : ℝ) =>
GlobalStressSupport.previousOmega (scheme W H Q M hlo) n (R, eta)) = 0
theorem
NavierStokes.EntranceAlignedBase.aligned_mass_primitive_zero
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
{n : ℕ}
(hn : 0 < n)
{p : ℝ × ℝ}
(hp : AssembledSlowBase.nominalOuterX W ≤ p.1)
(heta : |p.2| ≤ 1)
:
theorem
NavierStokes.EntranceAlignedBase.pressureCoefficient_zero
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
(n : ℕ)
{p : ℝ × ℝ}
(hX : 0 < p.1)
(heta : p.2 ∈ S)
:
SlowExpansionResidual.pressureCoefficient F.data.h W.axis.normalization
(GlobalSlowProfiles.asSlowProfiles (scheme W H Q M hlo)) n p = 0
theorem
NavierStokes.EntranceAlignedBase.aligned_finiteIdentities
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
:
BaseResidual.FiniteIdentities F.data.h W.axis.normalization (alignedCoefficients W H Q M hlo)
(GlobalSlowProfiles.asSlowProfiles (scheme W H Q M hlo))
theorem
NavierStokes.EntranceAlignedBase.zeroEnd_lt_outer
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{lo : ℝ}
(hlo : NominalConeAssembly.activeLeft W < lo)
:
theorem
NavierStokes.EntranceAlignedBase.zeroEnd_lt_outer_collar
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{lo : ℝ}
(hlo : NominalConeAssembly.activeLeft W < lo)
:
theorem
NavierStokes.EntranceAlignedBase.aligned_first_pair_eq
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
(hrow : ∀ eta ∈ S, Q.I (AssembledSlowBase.nominalOuterX W, eta) = W.profiles.I (AssembledSlowBase.nominalOuterX W, eta))
:
Set.EqOn (BaseResidual.stressPair (alignedCoefficients W H Q M hlo) 1)
(fun (p : SlowBorelBase.Inner) =>
(SlowFirstOrderEdge.stressX (FirstOrderBaseEdge.terminalAmplitude W) F.data (FirstOrderBaseEdge.terminalShift W) p, 0))
(Set.Ioi (FirstOrderBaseEdge.terminalInner W) ×ˢ Set.Ioo (-1) 1)
theorem
NavierStokes.EntranceAlignedBase.aligned_first_edgeJets
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
(hrow : ∀ eta ∈ S, Q.I (AssembledSlowBase.nominalOuterX W, eta) = W.profiles.I (AssembledSlowBase.nominalOuterX W, eta))
{c : ℝ}
(hc : 0 < c)
:
BaseResidual.PolynomialEdgeJets
(BaseResidual.outerWindow (Real.exp (ConstructedSlowBase.activeRight W - 1)) (ConstructedSlowBase.activeRight W))
(BaseResidual.activeZeta c (Real.log (NominalConeAssembly.activeLeft W)) (ConstructedSlowBase.activeRight W))
(BaseResidual.activeDelta (Real.log (NominalConeAssembly.activeLeft W)) (ConstructedSlowBase.activeRight W))
(BaseResidual.stressPair (alignedCoefficients W H Q M hlo) 1)
theorem
NavierStokes.EntranceAlignedBase.aligned_first_stress_zero_right
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
(hrow : ∀ eta ∈ S, Q.I (AssembledSlowBase.nominalOuterX W, eta) = W.profiles.I (AssembledSlowBase.nominalOuterX W, eta))
{p : ℝ × ℝ}
(hp : Real.exp (ConstructedSlowBase.activeRight W) ≤ p.1)
(heta : p.2 ∈ Set.Icc (-1) 1)
:
(alignedCoefficients W H Q M hlo).stressTheta 1 p = 0 ∧ (alignedCoefficients W H Q M hlo).stressAxial 1 p = 0
theorem
NavierStokes.EntranceAlignedBase.aligned_leading_stress_eq
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(H : NominalConeAssembly.Certificate W)
{D : ProfileHistories.RadialDomain}
(Q : ProfileHistories.Profiles D)
{S : Set ℝ}
{lo hi : ℝ}
(M : AssembledSlowBase.FiniteModification W Q S lo hi)
(hlo : NominalConeAssembly.activeLeft W < lo)
{p : ℝ × ℝ}
(hX : 0 ≤ p.1)
(heta : |p.2| ≤ 1)
(hf : ∀ (X : ℝ), 0 < X → X ≤ p.1 → Q.f (X, p.2) ≠ 0)
:
(alignedCoefficients W H Q M hlo).stressTheta 0 p = LeadingStress.theta Q F.data.h p ∧ (alignedCoefficients W H Q M hlo).stressAxial 0 p = LeadingStress.axial Q F.data.h p
theorem
NavierStokes.EntranceAlignedBase.exp_right_eq_cone
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
:
The unchanged terminal clock agrees exactly with the cone annulus.
theorem
NavierStokes.EntranceAlignedBase.modulation_after_entrance
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
{d : ModulatedProfileAssembly.LoopData W}
:
The actual finite modulation already supplies the required positive entrance margin; it is not an additional hypothesis on the final witness.
noncomputable def
NavierStokes.EntranceAlignedBase.modulatedScheme
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{d : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness d)
:
Modulated scheme, given by scheme W H v.profiles v.finiteModification (modulation_after_entrance (d := d)).
Equations
Instances For
noncomputable def
NavierStokes.EntranceAlignedBase.modulatedCoefficients
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{d : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness d)
:
Modulated coefficients, given by alignedCoefficients W H v.profiles v.finiteModification (modulation_after_entrance (d := d)).
Equations
Instances For
theorem
NavierStokes.EntranceAlignedBase.modulated_base_eq
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{d : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness d)
:
theorem
NavierStokes.EntranceAlignedBase.modulated_baseFields_eq
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{d : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness d)
:
theorem
NavierStokes.EntranceAlignedBase.modulated_outer
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{d : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness d)
:
theorem
NavierStokes.EntranceAlignedBase.modulated_phi_eq_extended
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{d : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness d)
(n : ℕ)
:
(modulatedCoefficients H v).phi n = AssembledSlowBase.extendedCoefficient (modulatedScheme H v) ⋯ n 0
theorem
NavierStokes.EntranceAlignedBase.modulated_axial_eq_extended
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{d : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness d)
(n : ℕ)
:
(modulatedCoefficients H v).axial n = AssembledSlowBase.extendedCoefficient (modulatedScheme H v) ⋯ n 1
theorem
NavierStokes.EntranceAlignedBase.modulated_pressure_eq_extended
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{d : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness d)
(n : ℕ)
:
(modulatedCoefficients H v).pressure n = AssembledSlowBase.extendedCoefficient (modulatedScheme H v) ⋯ n 3
theorem
NavierStokes.EntranceAlignedBase.modulated_smooth
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{d : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness d)
:
theorem
NavierStokes.EntranceAlignedBase.modulated_stressZeroCore
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{d : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness d)
:
theorem
NavierStokes.EntranceAlignedBase.modulated_positive_stress_zero
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{d : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness d)
{n : ℕ}
(hn : 0 < n)
{p : ℝ × ℝ}
(hp : p.1 ≤ zeroEnd W H d.modulation.left)
:
theorem
NavierStokes.EntranceAlignedBase.modulated_higherInteriorSupport
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{d : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness d)
:
theorem
NavierStokes.EntranceAlignedBase.modulated_zero_fields
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{d : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness d)
{p : ℝ × ℝ}
(hX : 0 ≤ p.1)
(heta : |p.2| ≤ 1)
:
(modulatedCoefficients H v).phi 0 p = W.axis.normalization * v.profiles.f p ∧ (modulatedCoefficients H v).axial 0 p = v.profiles.U p ∧ (modulatedCoefficients H v).pressure 0 p = v.profiles.pressure p
theorem
NavierStokes.EntranceAlignedBase.modulated_leading_stress_eq
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{d : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness d)
{p : ℝ × ℝ}
(hX : 0 ≤ p.1)
(heta : |p.2| ≤ 1)
:
(modulatedCoefficients H v).stressTheta 0 p = LeadingStress.theta v.profiles F.data.h p ∧ (modulatedCoefficients H v).stressAxial 0 p = LeadingStress.axial v.profiles F.data.h p
theorem
NavierStokes.EntranceAlignedBase.modulated_leading_pair_eq
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{d : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness d)
{p : ℝ × ℝ}
(hX : 0 ≤ p.1)
(heta : |p.2| ≤ 1)
:
BaseResidual.stressPair (modulatedCoefficients H v) 0 p = (LeadingStress.theta v.profiles F.data.h p, LeadingStress.axial v.profiles F.data.h p)
theorem
NavierStokes.EntranceAlignedBase.modulated_leading_axis
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{d : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness d)
{eta : ℝ}
(heta : eta ∈ Set.Icc (-1) 1)
:
theorem
NavierStokes.EntranceAlignedBase.modulated_positive_axis
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{d : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness d)
{n : ℕ}
(hn : 0 < n)
{eta : ℝ}
(heta : |eta| ≤ 1)
:
theorem
NavierStokes.EntranceAlignedBase.modulated_finiteIdentities
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{d : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness d)
:
theorem
NavierStokes.EntranceAlignedBase.modulated_first_edgeJets
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{d : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness d)
{c : ℝ}
(hc : 0 < c)
:
BaseResidual.PolynomialEdgeJets
(BaseResidual.outerWindow (Real.exp (ConstructedSlowBase.activeRight W - 1)) (ConstructedSlowBase.activeRight W))
(BaseResidual.activeZeta c (Real.log (NominalConeAssembly.activeLeft W)) (ConstructedSlowBase.activeRight W))
(BaseResidual.activeDelta (Real.log (NominalConeAssembly.activeLeft W)) (ConstructedSlowBase.activeRight W))
(BaseResidual.stressPair (modulatedCoefficients H v) 1)
theorem
NavierStokes.EntranceAlignedBase.modulated_positive_stress_zero_right
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{d : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness d)
{n : ℕ}
(hn : 0 < n)
{p : ℝ × ℝ}
(hp : NominalConeAssembly.activeRight W ≤ p.1)
(heta : p.2 ∈ Set.Icc (-1) 1)
:
theorem
NavierStokes.EntranceAlignedBase.modulated_positive_radialSupport
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{d : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness d)
{n : ℕ}
(hn : 0 < n)
:
SlowStressSupport.radialSupport (Set.Icc (-1) 1) (zeroEnd W H d.modulation.left) (NominalConeAssembly.activeRight W)
((modulatedCoefficients H v).stressTheta n) ∧ SlowStressSupport.radialSupport (Set.Icc (-1) 1) (zeroEnd W H d.modulation.left) (NominalConeAssembly.activeRight W)
((modulatedCoefficients H v).stressAxial n)
theorem
NavierStokes.EntranceAlignedBase.modulated_stress_zero_right
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{d : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness d)
(n : ℕ)
{p : ℝ × ℝ}
(hp : NominalConeAssembly.activeRight W ≤ p.1)
(heta : p.2 ∈ Set.Icc (-1) 1)
:
theorem
NavierStokes.EntranceAlignedBase.modulated_all_stress_support
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{d : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness d)
(n : ℕ)
:
SlowStressSupport.radialSupport (Set.Icc (-1) 1) (NominalConeAssembly.activeLeft W) (NominalConeAssembly.activeRight W)
((modulatedCoefficients H v).stressTheta n) ∧ SlowStressSupport.radialSupport (Set.Icc (-1) 1) (NominalConeAssembly.activeLeft W)
(NominalConeAssembly.activeRight W) ((modulatedCoefficients H v).stressAxial n)
Every actual coefficient, including orders zero and one, has support in the same true-cone annulus on the closed physical parameter band.
theorem
NavierStokes.EntranceAlignedBase.modulated_normalizedTensor_zero
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{d : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness d)
(a : ℕ → ℕ)
(q : ℝ)
{p : ℝ × ℝ}
(hp : p.1 ∉ Set.Icc (NominalConeAssembly.activeLeft W) (NominalConeAssembly.activeRight W))
(heta : p.2 ∈ Set.Icc (-1) 1)
:
The entire summed normalized tensor has the same support, for every cutoff schedule and every value of the expansion parameter.
theorem
NavierStokes.EntranceAlignedBase.modulated_transition_true
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{d : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness d)
{p : ℝ × ℝ}
(hp : p.1 ∈ Set.Icc (cutoffInner W H d.modulation.left) (cutoffStop W H d.modulation.left))
(heta : p.2 ∈ Set.Icc (-1) 1)
:
The transition lies in the true cone of the same final modulated profile, with its actual restored histories.
theorem
NavierStokes.EntranceAlignedBase.modulated_quotients_smooth
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{d : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness d)
{c : ℝ}
(hc : 0 < c)
(n : ℕ)
:
theorem
NavierStokes.EntranceAlignedBase.modulated_weighted_on_actual_scales
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{d : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness d)
{a : ℕ → ℕ}
{c : ℝ}
(hc : 0 < c)
{K : Set SlowBorelBase.Inner}
(hK : IsCompact K)
(hWK : BaseResidual.activeWindow (Real.log (NominalConeAssembly.activeLeft W)) (ConstructedSlowBase.activeRight W) ⊆ K)
(ha :
SlowBorelBase.AdmissibleScales F.data.h
(BaseResidual.weightedBundle W.axis.normalization (modulatedCoefficients H v)
(BaseResidual.activeZeta c (Real.log (NominalConeAssembly.activeLeft W)) (ConstructedSlowBase.activeRight W)))
K a)
:
The weighted estimate uses the true entrance, together with the proved interior support and the actual first-order terminal jets.
noncomputable def
NavierStokes.EntranceAlignedBase.scales
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{d : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness d)
(c : ℝ)
(hc : 0 < c)
(upper : ℝ)
(B : ℕ)
:
One common schedule is chosen after rebuilding the aligned coefficient family. It controls both the ordinary base and its weighted stress sum.
Equations
- NavierStokes.EntranceAlignedBase.scales H v c hc upper B = Classical.choose ⋯
Instances For
theorem
NavierStokes.EntranceAlignedBase.scales_spec
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{d : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness d)
(c : ℝ)
(hc : 0 < c)
(upper : ℝ)
(B : ℕ)
:
B ≤ scales H v c hc upper B 0 ∧ SlowBorelBase.AdmissibleScales F.data.h
(BaseResidual.weightedBundle W.axis.normalization (modulatedCoefficients H v)
(BaseResidual.activeZeta c (Real.log (NominalConeAssembly.activeLeft W)) (ConstructedSlowBase.activeRight W)))
(SlowBorelBase.innerBox 0 (ConstructedSlowBase.scaleUpper W upper)) (scales H v c hc upper B)
theorem
NavierStokes.EntranceAlignedBase.scales_admissible
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{d : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness d)
(c : ℝ)
(hc : 0 < c)
(upper : ℝ)
(B : ℕ)
:
SlowBorelBase.AdmissibleScales F.data.h
(SlowBorelBase.coefficientBundle W.axis.normalization (modulatedCoefficients H v))
(SlowBorelBase.innerBox 0 (ConstructedSlowBase.scaleUpper W upper)) (scales H v c hc upper B)
theorem
NavierStokes.EntranceAlignedBase.scales_strictMono
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{d : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness d)
(c : ℝ)
(hc : 0 < c)
(upper : ℝ)
(B : ℕ)
:
StrictMono (scales H v c hc upper B)
theorem
NavierStokes.EntranceAlignedBase.scales_weighted
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
(H : NominalConeAssembly.Certificate W)
{d : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness d)
(c : ℝ)
(hc : 0 < c)
(upper : ℝ)
(B : ℕ)
:
ConstructedSlowBase.WeightedStressBound (scales H v c hc upper B) F.data.h (modulatedCoefficients H v) c
(Real.log (NominalConeAssembly.activeLeft W)) (ConstructedSlowBase.activeRight W)
From the actual profile cone to the primary spectral cone #
The signed axial shear in the profile cone is c = -2 X U_X / E.
Consequently the physical shear vector is F * (-a,-c), while the
leading stress is a positive multiple of (p₁-a,p₂-c). The results
below derive the primary spectral and target cones from these identities.
Actual summed base fields in normalized band charts #
All coordinate derivatives are taken at strictly positive backward time. The constants remain uniform as that time approaches zero while the normalized positive branch stays in a fixed annulus.
noncomputable def
NavierStokes.BaseChartJets.oneDomain
(ι : Type u_1)
{E : Type u_2}
[NormedAddCommGroup E]
(U : ι → Set E)
(hU : ∀ (i : ι), IsOpen (U i))
:
One domain, bundling scale, carrier, isOpen, one_le_scale.
Equations
- NavierStokes.BaseChartJets.oneDomain ι U hU = { scale := fun (x : ι) => 1, carrier := U, isOpen := hU, one_le_scale := ⋯ }
Instances For
theorem
NavierStokes.BaseChartJets.uniform_polynomial
{ι : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{U : ι → Set E}
(hU : ∀ (i : ι), IsOpen (U i))
{f : ι → E → F}
(hs : ∀ (i : ι), ContDiffOn ℝ (↑⊤) (f i) (U i))
(hb : ∀ (j : ℕ), ∃ (C : ℝ), 0 < C ∧ ∀ (i : ι), ∀ x ∈ U i, ‖iteratedFDeriv ℝ j (f i) x‖ ≤ C)
:
PhaseJetBounds.PolynomialJets (oneDomain ι U hU) f
theorem
NavierStokes.BaseChartJets.uniform_envelope
{ι : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{U : ι → Set E}
(hU : ∀ (i : ι), IsOpen (U i))
{f : ι → E → F}
{w : ι → ℝ}
(hw : ∀ (i : ι), 0 ≤ w i)
(hs : ∀ (i : ι), ContDiffOn ℝ (↑⊤) (f i) (U i))
(hb : ∀ (j : ℕ), ∃ (C : ℝ), 0 < C ∧ ∀ (i : ι), ∀ x ∈ U i, ‖iteratedFDeriv ℝ j (f i) x‖ ≤ C * w i)
:
PrimaryPulseBounds.EnvelopeJets (oneDomain ι U hU) (fun (i : ι) (x : E) => w i) f
theorem
NavierStokes.BaseChartJets.scaled_jet_from_blown
{f : Chart → ℝ}
(hf : ContDiffOn ℝ (↑⊤) f sumRegion)
{Q rho M : ℝ}
{w : Inner}
(hQ : 0 < Q)
(hrho : 0 < rho)
(hw : 0 < w.1)
(hM : 1 ≤ M)
(hi : 1 / rho ≤ M)
(j : ℕ)
:
Recenter the frozen q-rescaling at the actual point q=Q*rho.
Only the bounded inverse of rho, not Q⁻¹, appears in this estimate.
theorem
NavierStokes.BaseChartJets.innerRegion_open
(qlo qhi lo hi : ℝ)
:
IsOpen (innerRegion qlo qhi lo hi)
theorem
NavierStokes.BaseChartJets.normalized_error_envelope
{ι : Type u_1}
{h qlo qhi lo hi : ℝ}
(hh : 0 < h)
(hqlo : 0 < qlo)
(hqhi : 0 < qhi)
(hlo : 0 < lo)
(Q : ι → ℝ)
(hQ : ∀ (i : ι), 0 < Q i)
(hsmall : ∀ (i : ι), Q i * qhi ≤ 1)
(f : Chart → ℝ)
(hf : ContDiffOn ℝ (↑⊤) f sumRegion)
(hb :
∀ (j : ℕ),
∃ (B : ℝ),
0 < B ∧ ∀ (q : ℝ),
0 < q → q ≤ 1 → ∀ w ∈ SlowBorelBase.innerBox lo hi, ‖SlowBorelBase.blownJet j f (q, w)‖ ≤ B * q ^ (2 * h))
:
PrimaryPulseBounds.EnvelopeJets (oneDomain ι (fun (x : ι) => innerRegion qlo qhi lo hi) ⋯)
(fun (i : ι) (x : Chart) => Q i ^ (2 * h)) fun (i : ι) => f ∘ ⇑(SlowBorelBase.scaleMap (Q i))
noncomputable def
NavierStokes.BaseChartJets.swirlError
(a : ℕ → ℕ)
(h C : ℝ)
(d : SlowBorelBase.Coefficients)
(y : Chart)
:
Swirl error, given by SlowBorelBase.normalizedSwirl a h C d y - SlowBorelBase.leadingSwirl C d y.2.
Equations
- NavierStokes.BaseChartJets.swirlError a h C d y = NavierStokes.SlowBorelBase.normalizedSwirl a h C d y - NavierStokes.SlowBorelBase.leadingSwirl C d y.2
Instances For
noncomputable def
NavierStokes.BaseChartJets.axialError
(a : ℕ → ℕ)
(h : ℝ)
(d : SlowBorelBase.Coefficients)
(y : Chart)
:
Axial error, given by SlowBorelBase.slowSum a h d.axial y - d.axial 0 y.2.
Equations
- NavierStokes.BaseChartJets.axialError a h d y = NavierStokes.SlowBorelBase.slowSum a h d.axial y - d.axial 0 y.2
Instances For
theorem
NavierStokes.BaseChartJets.errors_smooth
{a : ℕ → ℕ}
(ha : StrictMono a)
(h C : ℝ)
{d : SlowBorelBase.Coefficients}
(hd : SlowBorelBase.SmoothCoefficients d)
:
theorem
NavierStokes.BaseChartJets.actual_error_envelopes
{ι : Type u_1}
{a : ℕ → ℕ}
{h C qlo qhi lo hi : ℝ}
(hh : 0 < h)
(hqlo : 0 < qlo)
(hqhi : 0 < qhi)
(hlo : 0 < lo)
{d : SlowBorelBase.Coefficients}
(hd : SlowBorelBase.SmoothCoefficients d)
(ha : SlowBorelBase.AdmissibleScales h (SlowBorelBase.coefficientBundle C d) (SlowBorelBase.innerBox lo hi) a)
(Q : ι → ℝ)
(hQ : ∀ (i : ι), 0 < Q i)
(hsmall : ∀ (i : ι), Q i * qhi ≤ 1)
:
(PrimaryPulseBounds.EnvelopeJets (oneDomain ι (fun (x : ι) => innerRegion qlo qhi lo hi) ⋯)
(fun (i : ι) (x : Chart) => Q i ^ (2 * h)) fun (i : ι) => swirlError a h C d ∘ ⇑(SlowBorelBase.scaleMap (Q i))) ∧ PrimaryPulseBounds.EnvelopeJets (oneDomain ι (fun (x : ι) => innerRegion qlo qhi lo hi) ⋯)
(fun (i : ι) (x : Chart) => Q i ^ (2 * h)) fun (i : ι) => axialError a h d ∘ ⇑(SlowBorelBase.scaleMap (Q i))
Normalized coordinates, given by SlowBorelBase.physicalChart h (physicalInput p).
Equations
Instances For
theorem
NavierStokes.BaseChartJets.normalizedCoordinates_smoothAt
{h : ℝ}
(hh : 0 < h)
(hh1 : h < 1 / 2)
{p : Slow}
(hT : 0 < p.2.2)
:
ContDiffAt ℝ (↑⊤) (normalizedCoordinates h) p
structure
NavierStokes.BaseChartJets.GeometryBounds
{ι : Type u_1}
(D : PhaseJetBounds.Domain ι Slow)
(h r M qlo qhi lo hi : ℝ)
:
These are only pointwise geometric restrictions on the actual chart, not coordinate-derivative or base-field estimates.
- q_range (i : ι) (p : Slow) : p ∈ D.carrier i → qlo < (normalizedCoordinates h p).1 ∧ (normalizedCoordinates h p).1 < qhi
- x_range (i : ι) (p : Slow) : p ∈ D.carrier i → lo < (normalizedCoordinates h p).2.1 ∧ (normalizedCoordinates h p).2.1 < hi
Instances For
noncomputable def
NavierStokes.BaseChartJets.unitScale
{ι : Type u_1}
{E : Type u_2}
[NormedAddCommGroup E]
(D : PhaseJetBounds.Domain ι E)
:
Unit scale, given by oneDomain ι D.carrier D.isOpen.
Equations
Instances For
theorem
NavierStokes.BaseChartJets.physicalChart_jet_bound
{h : ℝ}
(hh : 0 < h)
(hh1 : h < 1 / 2)
(lo hi qhi : ℝ)
(j : ℕ)
:
∃ (C : ℝ),
0 < C ∧ ∀ (p : Chart),
p.1 < 1 →
(SlowBorelBase.physicalChart h p).1 ≤ qhi →
(SlowBorelBase.physicalChart h p).2.1 ∈ Set.Icc lo hi →
‖iteratedFDeriv ℝ j (SlowBorelBase.physicalChart h) p‖ ≤ C * (SlowBorelBase.physicalChart h p).1 ^ (-↑j)
The actual inverse coordinate jets are bounded for any fixed upper q bound. The proof uses the normalized inverse-Jacobian expressions, which are regular at the limiting forward parameters.
theorem
NavierStokes.BaseChartJets.normalizedCoordinates_polynomial
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r M qlo qhi lo hi : ℝ}
(hh : 0 < h)
(hh1 : h < 1 / 2)
(hqlo : 0 < qlo)
(H : GeometryBounds D h r M qlo qhi lo hi)
:
PhaseJetBounds.PolynomialJets (unitScale D) fun (x : ι) => normalizedCoordinates h
Uniform jets of (rho,X,eta) on strictly positive time. No lower
bound on time is imposed, and no derivative at time zero is used.
Axial factor, given by (normalizedCoordinates h p).1 ^ (-CoordinateAlgebra.A h).
Equations
Instances For
noncomputable def
NavierStokes.BaseChartJets.frequency
(a : ℕ → ℕ)
(h C : ℝ)
(d : SlowBorelBase.Coefficients)
(Q : ℝ)
(p : Slow)
:
The actual Q^A-normalized angular velocity divided by the normalized
radius. The factor 1/R is retained in the definition.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NavierStokes.BaseChartJets.axial
(a : ℕ → ℕ)
(h : ℝ)
(d : SlowBorelBase.Coefficients)
(Q : ℝ)
(p : Slow)
:
Axial, given by axialFactor h p * SlowBorelBase.slowSum a h d.axial (SlowBorelBase.scaleMap Q (normalizedCoordinates h p)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NavierStokes.BaseChartJets.leadingFrequency
(h C : ℝ)
(d : SlowBorelBase.Coefficients)
(p : Slow)
:
Leading frequency, given by frequencyFactor h p * SlowBorelBase.leadingSwirl C d (normalizedCoordinates h p).2.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NavierStokes.BaseChartJets.leadingAxial
(h : ℝ)
(d : SlowBorelBase.Coefficients)
(p : Slow)
:
Leading axial, given by axialFactor h p * d.axial 0 (normalizedCoordinates h p).2.
Equations
Instances For
theorem
NavierStokes.BaseChartJets.geometry_factors_polynomial
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r M qlo qhi lo hi : ℝ}
(hh : 0 < h)
(hh1 : h < 1 / 2)
(hr : 0 < r)
(hM : 1 ≤ M)
(hqlo : 0 < qlo)
(H : GeometryBounds D h r M qlo qhi lo hi)
:
(PhaseJetBounds.PolynomialJets (unitScale D) fun (x : ι) => frequencyFactor h) ∧ PhaseJetBounds.PolynomialJets (unitScale D) fun (x : ι) => axialFactor h
theorem
NavierStokes.BaseChartJets.leading_fields_polynomial
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{h r M qlo qhi lo hi C : ℝ}
(hh : 0 < h)
(hh1 : h < 1 / 2)
(hr : 0 < r)
(hM : 1 ≤ M)
(hqlo : 0 < qlo)
(hlo : 0 < lo)
(H : GeometryBounds D h r M qlo qhi lo hi)
{d : SlowBorelBase.Coefficients}
(hd : SlowBorelBase.SmoothCoefficients d)
:
(PhaseJetBounds.PolynomialJets (unitScale D) fun (x : ι) => leadingFrequency h C d) ∧ PhaseJetBounds.PolynomialJets (unitScale D) fun (x : ι) => leadingAxial h d
structure
NavierStokes.BaseChartJets.Estimates
{ι : Type u_1}
(D : PhaseJetBounds.Domain ι Slow)
(Q : ι → ℝ)
(a : ℕ → ℕ)
(h C : ℝ)
(d : SlowBorelBase.Coefficients)
:
All quantities in this conclusion are literal summed-field formulas.
- frequency_error : PrimaryPulseBounds.EnvelopeJets (unitScale D) (fun (i : ι) (x : Slow) => Q i ^ (2 * h)) fun (i : ι) (p : Slow) => frequency a h C d (Q i) p - leadingFrequency h C d p
- axial_error : PrimaryPulseBounds.EnvelopeJets (unitScale D) (fun (i : ι) (x : Slow) => Q i ^ (2 * h)) fun (i : ι) (p : Slow) => axial a h d (Q i) p - leadingAxial h d p
- leading_frequency : PhaseJetBounds.PolynomialJets (unitScale D) fun (x : ι) => leadingFrequency h C d
- leading_axial : PhaseJetBounds.PolynomialJets (unitScale D) fun (x : ι) => leadingAxial h d
- frequency_jets : PhaseJetBounds.PolynomialJets (unitScale D) fun (i : ι) => frequency a h C d (Q i)
- axial_jets : PhaseJetBounds.PolynomialJets (unitScale D) fun (i : ι) => axial a h d (Q i)
Instances For
theorem
NavierStokes.BaseChartJets.actual_estimates
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{a : ℕ → ℕ}
{h C r M qlo qhi lo hi : ℝ}
(hh : 0 < h)
(hh1 : h < 1 / 2)
(hr : 0 < r)
(hM : 1 ≤ M)
(hqlo : 0 < qlo)
(hqhi : 0 < qhi)
(hlo : 0 < lo)
(H : GeometryBounds D h r M qlo qhi lo hi)
{d : SlowBorelBase.Coefficients}
(hd : SlowBorelBase.SmoothCoefficients d)
(ha : SlowBorelBase.AdmissibleScales h (SlowBorelBase.coefficientBundle C d) (SlowBorelBase.innerBox lo hi) a)
(Q : ι → ℝ)
(hQ : ∀ (i : ι), 0 < Q i)
(hQ1 : ∀ (i : ι), Q i ≤ 1)
(hsmall : ∀ (i : ι), Q i * qhi ≤ 1)
:
Estimates D Q a h C d
theorem
NavierStokes.BaseChartJets.polynomial_unit_bound
{ι : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{D : PhaseJetBounds.Domain ι E}
{f : ι → E → F}
(hf : PhaseJetBounds.PolynomialJets (unitScale D) f)
(N : ℕ)
:
With unit bookkeeping scale, polynomial bounds are uniform bounds.
theorem
NavierStokes.BaseChartJets.envelope_unit_bound
{ι : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{D : PhaseJetBounds.Domain ι E}
{f : ι → E → F}
{w : ι → E → ℝ}
(hf : PrimaryPulseBounds.EnvelopeJets (unitScale D) w f)
(N : ℕ)
:
theorem
NavierStokes.BaseChartJets.polynomial_of_unit
{ι : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{D : PhaseJetBounds.Domain ι E}
{f : ι → E → F}
(hf : PhaseJetBounds.PolynomialJets (unitScale D) f)
:
theorem
NavierStokes.BaseChartJets.norm_fderiv_eq_jet_one
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
(f : E → F)
(x : E)
:
theorem
NavierStokes.BaseChartJets.norm_second_fderiv_eq_jet_two
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
(f : E → F)
(x : E)
:
theorem
NavierStokes.BaseChartJets.Estimates.polynomial_fields
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{Q : ι → ℝ}
{a : ℕ → ℕ}
{h C : ℝ}
{d : SlowBorelBase.Coefficients}
(H : Estimates D Q a h C d)
:
(PhaseJetBounds.PolynomialJets D fun (i : ι) => frequency a h C d (Q i)) ∧ PhaseJetBounds.PolynomialJets D fun (i : ι) => axial a h d (Q i)
theorem
NavierStokes.BaseChartJets.Estimates.localBaseBounds
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{Q : ι → ℝ}
{a : ℕ → ℕ}
{h C : ℝ}
{d : SlowBorelBase.Coefficients}
(H : Estimates D Q a h C d)
(hh : 0 ≤ h)
(hQ : ∀ (i : ι), 0 < Q i)
(hQ1 : ∀ (i : ι), Q i ≤ 1)
(hconvex : ∀ (i : ι), Convex ℝ (D.carrier i))
:
∃ (B : ℝ),
1 ≤ B ∧ ∀ (i : ι),
PhaseEstimates.LocalBaseBounds (frequency a h C d (Q i)) (axial a h d (Q i)) (leadingFrequency h C d)
(leadingAxial h d) (D.carrier i) B (Q i ^ h)
The actual all-order error estimates supply the precise C1/C2 input
of BasePhaseGeometry. The constant is chosen before the band or label.
theorem
NavierStokes.BaseChartJets.actual_localBase_and_polynomial
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{a : ℕ → ℕ}
{h C r M qlo qhi lo hi : ℝ}
(hh : 0 < h)
(hh1 : h < 1 / 2)
(hr : 0 < r)
(hM : 1 ≤ M)
(hqlo : 0 < qlo)
(hqhi : 0 < qhi)
(hlo : 0 < lo)
(H : GeometryBounds D h r M qlo qhi lo hi)
(hconvex : ∀ (i : ι), Convex ℝ (D.carrier i))
{d : SlowBorelBase.Coefficients}
(hd : SlowBorelBase.SmoothCoefficients d)
(ha : SlowBorelBase.AdmissibleScales h (SlowBorelBase.coefficientBundle C d) (SlowBorelBase.innerBox lo hi) a)
(Q : ι → ℝ)
(hQ : ∀ (i : ι), 0 < Q i)
(hQ1 : ∀ (i : ι), Q i ≤ 1)
(hsmall : ∀ (i : ι), Q i * qhi ≤ 1)
:
(PhaseJetBounds.PolynomialJets D fun (i : ι) => frequency a h C d (Q i)) ∧ (PhaseJetBounds.PolynomialJets D fun (i : ι) => axial a h d (Q i)) ∧ ∃ (B : ℝ),
1 ≤ B ∧ ∀ (i : ι),
PhaseEstimates.LocalBaseBounds (frequency a h C d (Q i)) (axial a h d (Q i)) (leadingFrequency h C d)
(leadingAxial h d) (D.carrier i) B (Q i ^ h)
Primitive summed-coefficient hypotheses, not supplied base estimates, produce both interfaces needed by the actual phase construction.
theorem
NavierStokes.BaseChartJets.leadingFrequency_eq
{h C : ℝ}
{d : SlowBorelBase.Coefficients}
(hh : 0 < h)
(hh1 : h < 1 / 2)
{p : Slow}
(hT : 0 < p.2.2)
(hR : 0 < p.1)
:
leadingFrequency h C d p = (normalizedCoordinates h p).1 ^ (-CoordinateAlgebra.A h - 1 / 2) / C * d.phi 0 (normalizedCoordinates h p).2
The leading angular frequency retains the 1/R factor; simplifying it
uses the actual relation X=R²/(2*rho).
theorem
NavierStokes.BaseChartJets.bandPoint_profile
{h Q : ℝ}
(hQ : 0 ≤ Q)
(p : Slow)
:
AxisymmetricFields.profilePoint (bandPoint h Q p).1 (bandPoint h Q p).2 = SimilarityHomogeneity.physicalScale h Q (physicalInput p)
theorem
NavierStokes.BaseChartJets.bandPoint_chart
{h Q : ℝ}
(hh : 0 < h)
(hh1 : h < 1 / 2)
(hQ : 0 < Q)
{p : Slow}
(hT : 0 < p.2.2)
:
SlowBorelBase.cartesianChart h (bandPoint h Q p) = (SlowBorelBase.scaleMap Q) (normalizedCoordinates h p)
theorem
NavierStokes.BaseChartJets.axial_eq_normalized_velocity
{a : ℕ → ℕ}
(ha : StrictMono a)
{h C Q : ℝ}
(hh : 0 < h)
(hh1 : h < 1 / 2)
(hQ : 0 < Q)
{d : SlowBorelBase.Coefficients}
(hd : SlowBorelBase.SmoothCoefficients d)
{p : Slow}
(hT : 0 < p.2.2)
:
axial a h d Q p = Q ^ CoordinateAlgebra.A h * (SlowBorelBase.baseVelocity a h C d (bandPoint h Q p)).ofLp 2
Literal equality with the axial component of the constructed curl base.
theorem
NavierStokes.BaseChartJets.frequency_eq_normalized_velocity
{a : ℕ → ℕ}
(ha : StrictMono a)
{h C Q : ℝ}
(hh : 0 < h)
(hh1 : h < 1 / 2)
(hQ : 0 < Q)
{d : SlowBorelBase.Coefficients}
(hd : SlowBorelBase.SmoothCoefficients d)
{p : Slow}
(hT : 0 < p.2.2)
(hR : 0 < p.1)
:
frequency a h C d Q p = Q ^ CoordinateAlgebra.A h * (SlowBorelBase.baseVelocity a h C d (bandPoint h Q p)).ofLp 1 / p.1
Literal equality with Q^A times the constructed angular velocity,
divided by the normalized radius.
theorem
NavierStokes.BaseChartJets.dyadic_actual_bounds
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{a : ℕ → ℕ}
{h C r M qlo qhi lo hi : ℝ}
(hh : 0 < h)
(hh1 : h < 1 / 2)
(hr : 0 < r)
(hM : 1 ≤ M)
(hqlo : 0 < qlo)
(hqhi : 0 < qhi)
(hlo : 0 < lo)
(H : GeometryBounds D h r M qlo qhi lo hi)
(hconvex : ∀ (i : ι), Convex ℝ (D.carrier i))
{d : SlowBorelBase.Coefficients}
(hd : SlowBorelBase.SmoothCoefficients d)
(ha : SlowBorelBase.AdmissibleScales h (SlowBorelBase.coefficientBundle C d) (SlowBorelBase.innerBox lo hi) a)
(band : ι → ℕ)
{N : ℕ}
(hN : ∀ n ≥ N, ChartScales.Q n * qhi ≤ 1)
(hband : ∀ (i : ι), N ≤ band i)
:
(PhaseJetBounds.PolynomialJets D fun (i : ι) => frequency a h C d (ChartScales.Q (band i))) ∧ (PhaseJetBounds.PolynomialJets D fun (i : ι) => axial a h d (ChartScales.Q (band i))) ∧ ∃ (B : ℝ),
1 ≤ B ∧ ∀ (i : ι),
PhaseEstimates.LocalBaseBounds (frequency a h C d (ChartScales.Q (band i)))
(axial a h d (ChartScales.Q (band i))) (leadingFrequency h C d) (leadingAxial h d) (D.carrier i) B
(ChartScales.epsilon h (band i))
Actual dyadic input interface. Indices may include every active label of every band above the one fixed cutoff.
theorem
NavierStokes.BaseChartJets.nominal_estimates
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{F : OutgoingProfile.Profile}
(W : NominalProfile.Witness F)
(c : ℝ)
(hc : 0 < c)
(upper : ℝ)
(B : ℕ)
{r M qlo qhi lo hi : ℝ}
(hr : 0 < r)
(hM : 1 ≤ M)
(hqlo : 0 < qlo)
(hqhi : 0 < qhi)
(hlo : 0 < lo)
(hhi : hi ≤ ConstructedSlowBase.scaleUpper W upper)
(H : GeometryBounds D F.data.h r M qlo qhi lo hi)
(Q : ι → ℝ)
(hQ : ∀ (i : ι), 0 < Q i)
(hQ1 : ∀ (i : ι), Q i ≤ 1)
(hsmall : ∀ (i : ι), Q i * qhi ≤ 1)
:
Estimates D Q (ConstructedSlowBase.nominalScales W c hc upper B) F.data.h W.axis.normalization
(AssembledSlowBase.nominalCoefficients W)
The already selected enlarged-bundle schedule of the nominal base instantiates the chart theorem without any additional schedule choice.
theorem
NavierStokes.BaseChartJets.modulated_estimates
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(c : ℝ)
(hc : 0 < c)
(upper : ℝ)
(B : ℕ)
{r M qlo qhi lo hi : ℝ}
(hr : 0 < r)
(hM : 1 ≤ M)
(hqlo : 0 < qlo)
(hqhi : 0 < qhi)
(hlo : 0 < lo)
(hhi : hi ≤ ConstructedSlowBase.scaleUpper W upper)
(H : GeometryBounds D F.data.h r M qlo qhi lo hi)
(Q : ι → ℝ)
(hQ : ∀ (i : ι), 0 < Q i)
(hQ1 : ∀ (i : ι), Q i ≤ 1)
(hsmall : ∀ (i : ι), Q i * qhi ≤ 1)
:
Estimates D Q (ConstructedSlowBase.Modulated.scales v c hc upper B) F.data.h W.axis.normalization
(ConstructedSlowBase.Modulated.coefficients v)
The same conclusion for the actual solved finite modulation and its single common weighted/ordinary Borel schedule.
theorem
NavierStokes.BaseChartJets.Estimates.uniform_errors
{ι : Type u_1}
{D : PhaseJetBounds.Domain ι Slow}
{Q : ι → ℝ}
{a : ℕ → ℕ}
{h C : ℝ}
{d : SlowBorelBase.Coefficients}
(H : Estimates D Q a h C d)
(N : ℕ)
:
A direct paired all-jet form, with constants uniform over every index of the chart family.
Every actual positive active label above a single fixed band.
Equations
- NavierStokes.BaseChartJets.CellIndex h lo hi N = { L : NavierStokes.PositiveRepresentatives.ActiveLabel (NavierStokes.PrimaryRepresentatives.referenceCompact h lo hi) // N ≤ (↑L).1 }
Instances For
noncomputable def
NavierStokes.BaseChartJets.cellBand
{h lo hi : ℝ}
{N : ℕ}
(L : CellIndex h lo hi N)
:
Cell band, given by L.val.val.1.
Equations
- NavierStokes.BaseChartJets.cellBand L = (↑↑L).1
Instances For
noncomputable def
NavierStokes.BaseChartJets.positiveCellDomain
(h lo hi : ℝ)
(N : ℕ)
:
PhaseJetBounds.Domain (CellIndex h lo hi N) Slow
The actual convex positive-time three-mesh cells. The slow scale is
precisely the manuscript's S_n; it is not a replacement coordinate.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.BaseChartJets.positiveCellDomain_convex
(h lo hi : ℝ)
(N : ℕ)
(L : CellIndex h lo hi N)
:
Convex ℝ ((positiveCellDomain h lo hi N).carrier L)
theorem
NavierStokes.BaseChartJets.positiveCellDomain_representative
(h lo hi : ℝ)
(N : ℕ)
(L : CellIndex h lo hi N)
:
PositiveRepresentatives.representative (PrimaryRepresentatives.referenceCompact h lo hi) ↑L ∈ (positiveCellDomain h lo hi N).carrier L
theorem
NavierStokes.BaseChartJets.positiveCellDomain_covers
(h lo hi : ℝ)
(N : ℕ)
(L : CellIndex h lo hi N)
:
PrimaryRepresentatives.gridBox (↑↑L).1 (↑↑L).2 2 ∩ PositiveRepresentatives.positiveTime ⊆
(positiveCellDomain h lo hi N).carrier L
theorem
NavierStokes.BaseChartJets.exists_actual_positive_charts
{a : ℕ → ℕ}
{h C lo hi : ℝ}
(hh : 0 < h)
(hh1 : h < 1 / 2)
(hlo : 0 < lo)
(hhi : lo ≤ hi)
{d : SlowBorelBase.Coefficients}
(hd : SlowBorelBase.SmoothCoefficients d)
(ha :
SlowBorelBase.AdmissibleScales h (SlowBorelBase.coefficientBundle C d) (SlowBorelBase.innerBox (lo / 2) (2 * hi)) a)
(N0 : ℕ)
:
∃ (N : ℕ),
N0 ≤ N ∧ Estimates (positiveCellDomain h lo hi N) (fun (L : CellIndex h lo hi N) => ChartScales.Q (cellBand L)) a h C d ∧ ∃ (B : ℝ),
1 ≤ B ∧ ∀ (L : CellIndex h lo hi N),
PhaseEstimates.LocalBaseBounds (frequency a h C d (ChartScales.Q (cellBand L)))
(axial a h d (ChartScales.Q (cellBand L))) (leadingFrequency h C d) (leadingAxial h d)
((positiveCellDomain h lo hi N).carrier L) B (ChartScales.epsilon h (cellBand L))
Full actual-input conclusion. The fixed annular profile and one admissible Borel schedule give all-order estimates and a single local-base constant on every actual enlarged positive-time cell above one band. No representative proximity, inverse-coordinate jets, or local-base estimates are hypotheses of this theorem.
theorem
NavierStokes.BaseChartJets.exists_modulated_positive_charts
{F : OutgoingProfile.Profile}
{W : NominalProfile.Witness F}
{ld : ModulatedProfileAssembly.LoopData W}
(v : ModulatedProfileAssembly.Witness ld)
(c : ℝ)
(hc : 0 < c)
(upper : ℝ)
(B0 : ℕ)
{lo hi : ℝ}
(hlo : 0 < lo)
(hhi : lo ≤ hi)
(hbox : 2 * hi ≤ ConstructedSlowBase.scaleUpper W upper)
(N0 : ℕ)
:
have a := ConstructedSlowBase.Modulated.scales v c hc upper B0;
have d := ConstructedSlowBase.Modulated.coefficients v;
∃ (N : ℕ),
N0 ≤ N ∧ Estimates (positiveCellDomain F.data.h lo hi N) (fun (L : CellIndex F.data.h lo hi N) => ChartScales.Q (cellBand L))
a F.data.h W.axis.normalization d ∧ ∃ (B : ℝ),
1 ≤ B ∧ ∀ (L : CellIndex F.data.h lo hi N),
PhaseEstimates.LocalBaseBounds (frequency a F.data.h W.axis.normalization d (ChartScales.Q (cellBand L)))
(axial a F.data.h d (ChartScales.Q (cellBand L))) (leadingFrequency F.data.h W.axis.normalization d)
(leadingAxial F.data.h d) ((positiveCellDomain F.data.h lo hi N).carrier L) B
(ChartScales.epsilon F.data.h (cellBand L))
Actual modulated base, actual common schedule, and actual positive active cells, combined in one theorem. The only annular restriction is that the selected schedule controls the enlarged fixed inner box.
theorem
NavierStokes.ProfileSpectralCone.referenceCone_of_trueCone
{F p₁ p₂ a c : ℝ}
(hF : 0 < F)
(h : TrueConeLoop.InTrueCone p₁ p₂ a c)
:
PrimaryRepresentatives.ReferenceCone F (F • !₂[-a, -c])
Projection of the actual stress coordinates onto the normal.
Projection onto the fixed transverse orientation -quarterTurn N.
theorem
NavierStokes.ProfileSpectralCone.spectral_cones_of_trueCone
{F τ p₁ p₂ a c : ℝ}
(hF : 0 < F)
(hτ : 0 < τ)
(h : TrueConeLoop.InTrueCone p₁ p₂ a c)
:
The true profile cone implies both primary cones, without assuming an eigenvector or target-cone inequality.
theorem
NavierStokes.ProfileSpectralCone.stress_coordinates_ne_zero
{p₁ p₂ a c : ℝ}
(h : TrueConeLoop.InTrueCone p₁ p₂ a c)
:
theorem
NavierStokes.ProfileSpectralCone.targetCone_of_signedShear
{F a c : ℝ}
(hF : 0 < F)
(ha : 0 < a)
(hv : 2 < a * (1 + (c / a) ^ 2))
(T : Plane)
(hin : 0 < a * T.ofLp 0 + c * T.ofLp 1)
(hquad : (a * (1 + (c / a) ^ 2) - 2) * (a * T.ofLp 1 - c * T.ofLp 0) ^ 2 < 2 * (a * T.ofLp 0 + c * T.ofLp 1) ^ 2)
:
PrimaryRepresentatives.TargetCone F (F • !₂[-a, -c]) T
A scalar criterion for any direction, including a nonzero smooth edge factor when the actual stress itself vanishes.
theorem
NavierStokes.ProfileSpectralCone.targetCone_of_tilt
{F a c : ℝ}
(hF : 0 < F)
(ha : 0 < a)
(hv : 2 < a * (1 + (c / a) ^ 2))
(T : Plane)
(hT : 0 < T.ofLp 0)
(hin : 0 < 1 + c / a * (T.ofLp 1 / T.ofLp 0))
(hgap :
0 < 2 * (1 + c / a * (T.ofLp 1 / T.ofLp 0)) ^ 2 - (a * (1 + (c / a) ^ 2) - 2) * (T.ofLp 1 / T.ofLp 0 - c / a) ^ 2)
:
PrimaryRepresentatives.TargetCone F (F • !₂[-a, -c]) T
The edge-collar convention uses the target tilt T₁ / T₀ and the
signed shear tilt c / a. Its two strict scalar margins imply the
primary target cone.
The actual profile histories and stresses #
noncomputable def
NavierStokes.ProfileSpectralCone.stressVector
{D : ProfileHistories.RadialDomain}
(P : ProfileHistories.Profiles D)
(h : ℝ)
(p : ProfileHistories.Point)
:
The two actual leading stress coefficients, in the Euclidean plane used by the primary ODE.
Equations
Instances For
theorem
NavierStokes.ProfileSpectralCone.stressVector_eq_stocks
{D : ProfileHistories.RadialDomain}
(P : ProfileHistories.Profiles D)
(h : ℝ)
{p : ProfileHistories.Point}
(hp : p ∈ D.carrier)
(hX : 0 < p.1)
(hf : P.f p ≠ 0)
:
stressVector P h p = P.f p • !₂[ActivationStocks.profileStockOne P h p - ModulatedCone.angularShear P.E p, ActivationStocks.profileStockTwo P h p - ModulatedCone.signedAxialShear P.E P.U p]
Both entries use the actual integral-history stocks; the axial sign agrees with the modulation convention.
theorem
NavierStokes.ProfileSpectralCone.profile_spectral_cones
{D : ProfileHistories.RadialDomain}
(P : ProfileHistories.Profiles D)
(h : ℝ)
{p : ProfileHistories.Point}
(hp : p ∈ D.carrier)
(hX : 0 < p.1)
(hf : 0 < P.f p)
{F : ℝ}
(hF : 0 < F)
(hc :
TrueConeLoop.InTrueCone (ActivationStocks.profileStockOne P h p) (ActivationStocks.profileStockTwo P h p)
(ModulatedCone.angularShear P.E p) (ModulatedCone.signedAxialShear P.E P.U p))
:
PrimaryRepresentatives.ReferenceCone F
(F • !₂[-ModulatedCone.angularShear P.E p, -ModulatedCone.signedAxialShear P.E P.U p]) ∧ PrimaryRepresentatives.TargetCone F
(F • !₂[-ModulatedCone.angularShear P.E p, -ModulatedCone.signedAxialShear P.E P.U p]) (stressVector P h p)
The actual leading stress belongs to the primary target cone whenever the actual five-history profile has the true cone.
theorem
NavierStokes.ProfileSpectralCone.profile_stress_ne_zero
{D : ProfileHistories.RadialDomain}
(P : ProfileHistories.Profiles D)
(h : ℝ)
{p : ProfileHistories.Point}
(hp : p ∈ D.carrier)
(hX : 0 < p.1)
(hf : 0 < P.f p)
(hc :
TrueConeLoop.InTrueCone (ActivationStocks.profileStockOne P h p) (ActivationStocks.profileStockTwo P h p)
(ModulatedCone.angularShear P.E p) (ModulatedCone.signedAxialShear P.E P.U p))
:
Genuine radial derivatives of the normalized leading fields #
theorem
NavierStokes.ProfileSpectralCone.normalizedCoordinates_radial
(h : ℝ)
(p : Slow)
(R : ℝ)
:
BaseChartJets.normalizedCoordinates h (R, p.2) = ((BaseChartJets.normalizedCoordinates h p).1, R ^ 2 / 2 / (BaseChartJets.normalizedCoordinates h p).1, (BaseChartJets.normalizedCoordinates h p).2.2)
theorem
NavierStokes.ProfileSpectralCone.leadingFrequency_germ
{h C : ℝ}
{d : SlowBorelBase.Coefficients}
(hh : 0 < h)
(hh1 : h < 1 / 2)
{p : Slow}
(hT : 0 < p.2.2)
(hR : 0 < p.1)
:
BaseChartJets.leadingFrequency h C d =ᶠ[nhds p] fun (q : Slow) =>
(BaseChartJets.normalizedCoordinates h q).1 ^ (-CoordinateAlgebra.A h - 1 / 2) / C * d.phi 0 (BaseChartJets.normalizedCoordinates h q).2
theorem
NavierStokes.ProfileSpectralCone.leadingFrequency_smoothAt
{h C : ℝ}
{d : SlowBorelBase.Coefficients}
(hh : 0 < h)
(hh1 : h < 1 / 2)
(hd : SlowBorelBase.SmoothCoefficients d)
{p : Slow}
(hT : 0 < p.2.2)
(hR : 0 < p.1)
:
ContDiffAt ℝ (↑⊤) (BaseChartJets.leadingFrequency h C d) p
theorem
NavierStokes.ProfileSpectralCone.leadingAxial_smoothAt
{h : ℝ}
{d : SlowBorelBase.Coefficients}
(hh : 0 < h)
(hh1 : h < 1 / 2)
(hd : SlowBorelBase.SmoothCoefficients d)
{p : Slow}
(hT : 0 < p.2.2)
:
ContDiffAt ℝ (↑⊤) (BaseChartJets.leadingAxial h d) p
theorem
NavierStokes.ProfileSpectralCone.leadingFrequency_slowR
{h C : ℝ}
{d : SlowBorelBase.Coefficients}
(hh : 0 < h)
(hh1 : h < 1 / 2)
(hd : SlowBorelBase.SmoothCoefficients d)
{p : Slow}
(hT : 0 < p.2.2)
(hR : 0 < p.1)
:
PhaseCalculus.slowR (BaseChartJets.leadingFrequency h C d) p = (BaseChartJets.normalizedCoordinates h p).1 ^ (-CoordinateAlgebra.A h - 1 / 2) / C * (p.1 / (BaseChartJets.normalizedCoordinates h p).1 * SimilarityProfile.partialX (d.phi 0) (BaseChartJets.normalizedCoordinates h p).2)
This is the Fréchet radial derivative of the actual leading angular frequency, with all chart scale factors retained.
theorem
NavierStokes.ProfileSpectralCone.leadingAxial_slowR
{h : ℝ}
{d : SlowBorelBase.Coefficients}
(hh : 0 < h)
(hh1 : h < 1 / 2)
(hd : SlowBorelBase.SmoothCoefficients d)
{p : Slow}
(hT : 0 < p.2.2)
:
PhaseCalculus.slowR (BaseChartJets.leadingAxial h d) p = (BaseChartJets.normalizedCoordinates h p).1 ^ (-CoordinateAlgebra.A h) * (p.1 / (BaseChartJets.normalizedCoordinates h p).1 * SimilarityProfile.partialX (d.axial 0) (BaseChartJets.normalizedCoordinates h p).2)
theorem
NavierStokes.ProfileSpectralCone.normalized_X_eq
(h : ℝ)
(p : Slow)
:
(BaseChartJets.normalizedCoordinates h p).2.1 = p.1 ^ 2 / (2 * (BaseChartJets.normalizedCoordinates h p).1)
theorem
NavierStokes.ProfileSpectralCone.leading_shear_eq_profile
{D : ProfileHistories.RadialDomain}
(P : ProfileHistories.Profiles D)
{h C : ℝ}
{d : SlowBorelBase.Coefficients}
(hh : 0 < h)
(hh1 : h < 1 / 2)
(hC : C ≠ 0)
(hd : SlowBorelBase.SmoothCoefficients d)
{p : Slow}
(hT : 0 < p.2.2)
(hR : 0 < p.1)
(hp : (BaseChartJets.normalizedCoordinates h p).2 ∈ D.carrier)
(hf : P.f (BaseChartJets.normalizedCoordinates h p).2 ≠ 0)
(hphi :
(fun (X : ℝ) =>
d.phi 0 (X, (BaseChartJets.normalizedCoordinates h p).2.2)) =ᶠ[nhds (BaseChartJets.normalizedCoordinates h p).2.1] fun (X : ℝ) => C * P.f (X, (BaseChartJets.normalizedCoordinates h p).2.2))
(hU :
(fun (X : ℝ) =>
d.axial 0
(X, (BaseChartJets.normalizedCoordinates h p).2.2)) =ᶠ[nhds (BaseChartJets.normalizedCoordinates h p).2.1] fun (X : ℝ) => P.U (X, (BaseChartJets.normalizedCoordinates h p).2.2))
:
PhaseEstimates.shearVector (BaseChartJets.leadingFrequency h C d) (BaseChartJets.leadingAxial h d) p = BaseChartJets.leadingFrequency h C d p • !₂[-ModulatedCone.angularShear P.E (BaseChartJets.normalizedCoordinates h p).2, -ModulatedCone.signedAxialShear P.E P.U (BaseChartJets.normalizedCoordinates h p).2]
Value and radial-germ agreement with a profile suffice to identify the genuine shear vector of the coefficient-defined leading fields.
Uniform choices on a compact reference set #
theorem
NavierStokes.ProfileSpectralCone.signedShear_continuousOn
{K : Set Slow}
{F a c : Slow → ℝ}
(hF : ContinuousOn F K)
(ha : ContinuousOn a K)
(hc : ContinuousOn c K)
:
theorem
NavierStokes.ProfileSpectralCone.compact_signedShear_bounds
{K : Set Slow}
(hK : IsCompact K)
{F a c : Slow → ℝ}
{T : Slow → Plane}
(hF : ContinuousOn F K)
(ha : ContinuousOn a K)
(hc : ContinuousOn c K)
(hT : ContinuousOn T K)
(hR : ∀ p ∈ K, 0 < p.1)
(hFp : ∀ p ∈ K, 0 < F p)
(hap : ∀ p ∈ K, 0 < a p)
(hv : ∀ p ∈ K, 2 < a p * (1 + (c p / a p) ^ 2))
(hin : ∀ p ∈ K, 0 < a p * (T p).ofLp 0 + c p * (T p).ofLp 1)
(hquad :
∀ p ∈ K,
(a p * (1 + (c p / a p) ^ 2) - 2) * (a p * (T p).ofLp 1 - c p * (T p).ofLp 0) ^ 2 < 2 * (a p * (T p).ofLp 0 + c p * (T p).ofLp 1) ^ 2)
:
∃ (M : ℝ) (u : ℝ) (eta : ℝ) (delta : ℝ),
1 ≤ M ∧ 0 < u ∧ 0 < eta ∧ 0 < delta ∧ (∀ p ∈ K,
PrimaryRepresentatives.ReferenceCone (F p) (F p • !₂[-a p, -c p]) ∧ PrimaryRepresentatives.TargetCone (F p) (F p • !₂[-a p, -c p]) (T p) ∧ PrimaryRepresentatives.ParameterBounds M p.1 (F p) (F p • !₂[-a p, -c p])) ∧ ∀ p₀ ∈ K,
∀ p ∈ K,
dist p p₀ < delta →
inner ℝ (T p) (PrimaryRepresentatives.normalDirection (F p₀ • !₂[-a p₀, -c p₀])) ≤ -eta ∧ |PrimaryRepresentatives.c0 (F p₀) (F p₀ • !₂[-a p₀, -c p₀]) * inner ℝ (T p) (PrimaryRepresentatives.transverseDirection (F p₀ • !₂[-a p₀, -c p₀])) / inner ℝ (T p) (PrimaryRepresentatives.normalDirection (F p₀ • !₂[-a p₀, -c p₀]))| + eta ≤ PrimaryRepresentatives.slopeRatio u
Scalar shear and direction margins on a compact set produce all
reference bounds and one mixed-point target margin. All constants are
chosen before a band or label is selected. T can be an extended edge
direction: no positive lower bound for a separate amplitude is used.
theorem
NavierStokes.ProfileSpectralCone.weighted_target_margin
{F eta u zeta : ℝ}
{g T : Plane}
(hz : 0 ≤ zeta)
(hin : inner ℝ T (PrimaryRepresentatives.normalDirection g) ≤ -eta)
(hratio : PrimaryRepresentatives.targetRatio F g T + eta ≤ PrimaryRepresentatives.slopeRatio u)
:
inner ℝ (zeta • T) (PrimaryRepresentatives.normalDirection g) ≤ -eta * zeta ∧ (0 < zeta → PrimaryRepresentatives.targetRatio F g (zeta • T) + eta ≤ PrimaryRepresentatives.slopeRatio u)
A vanishing nonnegative amplitude preserves the linear inward margin; where it is positive it cancels exactly from the target ratio.