Positive-time regularity and material derivative for the actual H_m source, packaged for the per-time transported energy assembler.

@[reducible, inline]

abbrev AVenhance.Infra.Section4.HmPerTimeRegularity.hmPerTimePositiveDomain : Set (ℝ × Homogenization.Vec 2)

Joint time-space domain with strictly positive time.

Equations

• AVenhance.Infra.Section4.HmPerTimeRegularity.hmPerTimePositiveDomain = Set.Ioi 0 ×ˢ Set.univ

theorem AVenhance.Infra.Section4.HmPerTimeRegularity.hmPerTime_stDiv_contDiffOn {p : ℕ} {F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2} (hF : ContDiffOn ℝ (↑p + 1) F hmPerTimePositiveDomain) : ContDiffOn ℝ (↑p) (Section5.stDiv F) hmPerTimePositiveDomain

theorem AVenhance.Infra.Section4.HmPerTimeRegularity.hmPerTime_endpoint_continuousOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κ κprev : ℝ} (hκ : 0 < κ) {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {Titer : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hT : I.IsTIterates hΦ m κ κprev θ₀ θprev Titer) (r : ℕ) (hbudget : ∀ n ∈ Finset.range (Nstar β), 2 + r ≤ Nstar β) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => Section5.hmEndpoint I hΦ m κ (Titer (Nstar β)) r p.1 p.2) hmPerTimePositiveDomain

theorem AVenhance.Infra.Section4.HmPerTimeRegularity.hmPerTime_terminalFlux_differentiable {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κ κprev : ℝ} (hκ : 0 < κ) {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {Titer : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hT : I.IsTIterates hΦ m κ κprev θ₀ θprev Titer) {t : ℝ} (ht : 0 < t) (x : Homogenization.Vec 2) : DifferentiableAt ℝ (hmFrozenTerminalFlux I hΦ m κ (Titer (Nstar β)) t) x

theorem AVenhance.Infra.Section4.HmPerTimeRegularity.hmPerTime_joint_flowMap_continuous {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) : Continuous fun (p : ℝ × Homogenization.Vec 2) => (p.1, I.xFlow hΦ m 0 p.1 p.2)

theorem AVenhance.Infra.Section4.HmPerTimeRegularity.hmPerTime_flowMap_mem {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} {p : ℝ × Homogenization.Vec 2} (hp : p ∈ Set.Ioi 0 ×ˢ Set.univ) : (p.1, I.xFlow hΦ m 0 p.1 p.2) ∈ Set.Ioi 0 ×ˢ Set.univ

theorem AVenhance.Infra.Section4.HmPerTimeRegularity.hmPerTime_regularFlux_periodic {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) {t : ℝ} (hTper : IsZ2Periodic (T t)) : IsZ2Periodic (hmFrozenRegularFlux I hΦ m κ T t)

The regular Piola flux is spatially periodic at positive times.

theorem AVenhance.Infra.Section4.HmPerTimeRegularity.hmPerTime_piolaSource_periodic {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) {t : ℝ} (hT : ContDiff ℝ (↑⊤) (T t)) (hTper : IsZ2Periodic (T t)) : IsZ2Periodic (hmFrozenPiolaSource I hΦ m κ T t)

The divergence of the regular Piola flux is spatially periodic.

theorem AVenhance.Infra.Section4.hm_positive_time_actual_regular_data {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κ κprev : ℝ} (hκ : 0 < κ) {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {Titer : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hT : I.IsTIterates hΦ m κ κprev θ₀ θprev Titer) : have T := Titer (Nstar β); have X := fun (t : ℝ) => Section5.LeftToShow.xFlowDiffeo I hΦ m 0 t; (∀ (t : ℝ), 0 < t → IsZ2Periodic (I.Hm hΦ m κ T t)) ∧ (∀ (t : ℝ), 0 < t → IsZ2Periodic fun (x : Homogenization.Vec 2) => hmFrozenPiolaSource I hΦ m κ T t x + vecDiv (Section5.sourceErrorD I hΦ m κ T t) x) ∧ (∀ (t : ℝ), 0 < t → ∀ (i : Fin 2), IsZ2Periodic fun (x : Homogenization.Vec 2) => Section5.sourceErrorD I hΦ m κ T t x i) ∧ (∀ (a b : ℝ), 0 < a → a ≤ b → ContinuousOn hmRegularPairing (Set.Icc a b) ∧ ContinuousOn hmFluxPairing (Set.Icc a b)) ∧ ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => I.Hm hΦ m κ T p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ) ∧ ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => hmFrozenPiolaSource I hΦ m κ T p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ) ∧ ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => vecDiv (Section5.sourceErrorD I hΦ m κ T p.1) p.2) (Set.Ioi 0 ×ˢ Set.univ) ∧ (∀ (t : ℝ), 0 < t → ContDiff ℝ 1 (I.Hm hΦ m κ T t)) ∧ (∀ (t : ℝ), 0 < t → Continuous (hmFrozenPiolaSource I hΦ m κ T t)) ∧ (∀ (t : ℝ), 0 < t → ContDiff ℝ 1 (Section5.sourceErrorD I hΦ m κ T t)) ∧ ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => I.Hm hΦ m κ T p.1 ((X p.1).toFun p.2)) (Set.Ioi 0 ×ˢ Set.univ) ∧ ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => (fun (x : Homogenization.Vec 2) => hmFrozenPiolaSource I hΦ m κ T p.1 x + vecDiv (Section5.sourceErrorD I hΦ m κ T p.1) x) ((X p.1).toFun p.2)) (Set.Ioi 0 ×ˢ Set.univ) ∧ (∀ (t : ℝ), 0 < t → ∀ (x : Homogenization.Vec 2), HasDerivAt (fun (s : ℝ) => I.Hm hΦ m κ T s ((X s).toFun x)) ((fun (y : Homogenization.Vec 2) => hmFrozenPiolaSource I hΦ m κ T t y + vecDiv (Section5.sourceErrorD I hΦ m κ T t) y) ((X t).toFun x)) t) ∧ ∀ (l : ℝ → ℤ), (∀ t ∈ Set.Ioc 0 1, 0 < hmHalfCellEndpointAt I m l t) → ∀ t ∈ Set.Ioc 0 1, ContinuousOn (fun (s : ℝ) => √(l2NormSq (I.Hm hΦ m κ T s))) (Set.Icc (min (hmHalfCellEndpointAt I m l t) t) (max (hmHalfCellEndpointAt I m l t) t))

The positive-time regularity and transport data needed by frozen_hm_positive_time_bounds_of_pairings_per_time, for the actual terminal iterate. The pairing and quantitative bounds remain explicit arguments of that assembler.