Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Section4.IteratesTruncatedCell

Terminal-time cells and monotonicity of actual nonnegative energies.

source
def AVenhance.Infra.Section4.iterateTruncatedCell (s : ℝ) :
Set AmnrSpace

The actual open time cell up to a specified terminal time.

Equations
Instances For
    source
    theorem AVenhance.Infra.Section4.iterateTruncatedCell_isOpen (s : ℝ) :
    IsOpen (iterateTruncatedCell s)

    The terminal cell is open for the actual positive-time calculus.

    source
    theorem AVenhance.Infra.Section4.iterateTruncatedCell_subset {s : ℝ} (hs : s ≤ 1) :
    iterateTruncatedCell s ⊆ timeCube

    Every terminal time in the interval gives a subcell.

    source
    theorem AVenhance.Infra.Section4.iterate_truncated_cell_integrable {f : AmnrSpace → ℝ} (hf : ContinuousOn f (Set.Ici 0 ×ˢ Set.univ)) {s : ℝ} (hs : 0 ≤ s) :
    MeasureTheory.IntegrableOn f (iterateTruncatedCell s) MeasureTheory.volume

    Continuous actual fields are integrable on every nonnegative terminal cell.

    source
    theorem AVenhance.Infra.Section4.iterate_truncated_nonnegative_integral_le {f : AmnrSpace → ℝ} (hi : MeasureTheory.IntegrableOn f timeCube MeasureTheory.volume) (hf : ∀ (z : AmnrSpace), 0 ≤ f z) {s : ℝ} (hs : s ≤ 1) :
    ∫ (z : AmnrSpace) in iterateTruncatedCell s, f z ≤ ∫ (z : ℝ × Homogenization.Vec 2) in timeCube, f z

    Nonnegative energy on a terminal cell is bounded by full-cell energy. This applies to energies, not signed pairings.

    source
    theorem AVenhance.Infra.Section4.iterate_truncated_integral_eq_interval {f : AmnrSpace → ℝ} (hf : ContinuousOn f (Set.Ici 0 ×ˢ Set.univ)) {s : ℝ} (hs : 0 ≤ s) :
    ∫ (z : AmnrSpace) in iterateTruncatedCell s, f z = ∫ (t : ℝ) in 0..s, ∫ (x : Homogenization.Vec 2) in unitCube, f (t, x)

    Fubini identifies each terminal cell with the actual time integral.

    source
    theorem AVenhance.Infra.Section4.iterate_truncated_integral_abs_le {f : AmnrSpace → ℝ} (hi : MeasureTheory.IntegrableOn f timeCube MeasureTheory.volume) {s : ℝ} (hs : s ≤ 1) :
    |∫ (z : AmnrSpace) in iterateTruncatedCell s, f z| ≤ ∫ (z : ℝ × Homogenization.Vec 2) in timeCube, |f z|

    A terminal signed integral is controlled by the full integral of the absolute value; no cancellation in the full signed integral is used.

    source
    theorem AVenhance.Infra.Section4.iterate_truncated_integral_eq_interval_of_integrable {f : AmnrSpace → ℝ} (hf : MeasureTheory.IntegrableOn f timeCube MeasureTheory.volume) {s : ℝ} (hs : 0 ≤ s) (hs1 : s ≤ 1) :
    ∫ (z : AmnrSpace) in iterateTruncatedCell s, f z = ∫ (t : ℝ) in 0..s, ∫ (x : Homogenization.Vec 2) in unitCube, f (t, x)

    Fubini also applies to actual positive-time pairings with an integrable initial-time representative, without initial-time continuity of the pairing.