OAI/NumberTheory/Ostmann/Construction/FixedPivotEnergyTransport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.scheduledReplacePivot line 11
2. theorem OAI.Ostmann.scheduledReplacePivot_wordLeafScale line 16

   Source documentation

   Replacing the current pivot never changes a selected original word prime.

   theorem scheduledReplacePivot_wordLeafScale {I : Type*}
       (role : I → CopyScheduleRole) (i : I) (hi : role i = .word) (n M : ℕ)
       (base : CopyScheduleAtoms role n → ℕ) (x : TreeLeafIndex n → ℕ) :
       scheduledReplacePivot role n M (wordLeafScale role i hi n base x) =
         wordLeafScale role i hi n (scheduledReplacePivot role n M base) x := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.scheduledReplacePivot, OAI.Ostmann.wordLeafScale

3. theorem OAI.Ostmann.scheduledReplacePivot_eq_inserted line 31

   Source documentation

   The replaced assignment is exactly the original H/Y assignment with M inserted.

   theorem scheduledReplacePivot_eq_inserted {I : Type*}
       (role : I → CopyScheduleRole) (n M : ℕ) (base : CopyScheduleAtoms role n → ℕ) :
       scheduledReplacePivot role n M base = scheduledInsertedAtoms role n M
         (fun h => base ⟨h.val, h.property.1⟩) (fun y => base ⟨y.val, y.property.1⟩) := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.scheduledReplacePivot, OAI.Ostmann.scheduledInsertedAtoms

4. theorem OAI.Ostmann.constituent_fixedPivot_energy_transport line 61

   Source documentation

   The full original product prior can be retained while the pivot is fixed externally. Its unused prime coordinates integrate out with total mass one.

   theorem constituent_fixedPivot_energy_transport {I D : Type*} [Fintype I] [Fintype D]
       (role : I → CopyScheduleRole) (size : I → ℕ)
       (i : Σ a, Fin (size a)) (hi : role i.1 = .word) (n M : ℕ)
       (P : Finset ℕ) (cells : (Σ a, Fin (size a)) → Finset ℕ)
       (hsub : ∀ j, cells j ⊆ P) (hmass : ∀ j, (∑ p ∈ cells j, (p : ℝ)⁻¹) ≠ 0)
       (F : D → (CopyScheduleAtoms role n → ℕ) → ℝ) (B : ℝ)
       (hsection : ∀ base : CopyScheduleAtoms role n → ℕ,
         (∑ d, ∑ x : TreeLeafIndex n → P, (∏ t, primeSubsetPrior P (cells i) (x t)) *
           F d (wordLeafScale role i.1 hi n base (fun t => (x t : ℕ)))) ≤ B) :
       (∑ d, ∑ q : SurvivingConstituent role size n → P,
         scheduledPrimePrior (fun j : Σ a, Fin (size a) => role j.1) n
           (fun j => primeSubsetPrior P (cells j)) q *
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.primeSubsetPrior, OAI.Ostmann.wordLeafScale, OAI.Ostmann.SurvivingConstituent, OAI.Ostmann.scheduledPrimePrior